Examples 2.1 and 4.1

module ex4-1 where

open import map
open import nat using (2Nat ; 5Nat)
open import bool using (true[] ; false[])
open import seq using (Seq[_] ; ⊢Seq ; pair[_,_] ; const[_])
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 

Γβ₁ : type-context {mix-var}
Γβ₁ = ⟦ [| β₁ |] ⟧

f : mix-var
f = fvar 

We then define the term of Example 2.1, and the specification with respect to which we are considering it.

t : term-expr
t = pair[ pair[ const[ true[] ] , const[ 2Nat ] ] , const[ 5Nat ] ]

⊢Seq[β₁] : Γβ₁ ∥ ∅ ⊢ Seq[ varᵀ β₁ ]
⊢Seq[β₁] = ⊢Seq (var-intro ∋-last)

C,s = adm t ⊢Seq[β₁] [| varᵀ f |] (record { curr =  }) []