This file finds the morphisms mappable over the list of lists [[1,2],[3]] when considered with respect to the specification List[List[β₁]]. Note that the inner lists are required, and the data in them are the elements of type ℕ.
module ex4-5 where open import map open import nat using (1Nat ; 2Nat ; 3Nat) open import list using (List[_] ; ⊢List ; nil[] ; cons[_,_] ) 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.5, and the specification with respect to which we are considering it.
t = cons[ cons[ 1Nat , cons[ 2Nat , nil[] ] ] , cons[ cons[ 3Nat , nil[] ] , nil[] ] ]
⊢ListList[β₁] : Γβ₁ ∥ ∅ ⊢ List[ List[ varᵀ β₁ ] ]
⊢ListList[β₁] = ⊢List (⊢List (var-intro ∋-last))
C,s = adm t ⊢ListList[β₁] [| varᵀ f |] (record { curr = 1 }) []