module ex4-2 where open import map open import nat using (2Nat ; 5Nat) open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_] ) open import G using (G[_] ; ⊢G ; const[] ; flat[_] ; inj[_] ; pairing[_,_] ; projpair[_]) open import Data.List using ([] ; _∷_ ; [_]) open import Data.Vec renaming ([] to [||] ; _∷_ to _¦_ ; [_] to [|_|] )
We start with the declaration of variables that will be used in the call to adm.
β₁ : mix-var
β₁ = tvar 0
Γβ₁ : type-context {mix-var}
Γβ₁ = ⟦ [| β₁ |] ⟧
f : mix-var
f = fvar 0
We then define the term of Example 2.2, and the specification with respect to which we are considering it.
t : term-expr
t = projpair[ inj[ inj[ cons[ 2Nat , nil[] ] ] , pairing[ inj[ 2Nat ] , const[] ] ] ]
⊢G[β₁] : Γβ₁ ∥ ∅ ⊢ G[ varᵀ β₁ ]
⊢G[β₁] = ⊢G (var-intro ∋-last)
C,s = adm t ⊢G[β₁] [| varᵀ f |] (record { curr = 1 }) []