| Parents |
| gst-fun |
| Constants |
|
nil
|
GS |
|
cons
|
GS → GS → GS |
|
list
|
GS LIST → GS |
|
tail
|
GS → GS |
|
head
|
GS → GS |
|
nth
|
ℕ → GS → GS |
| Definitions |
|
nil
|
⊢ nil = ∅g |
|
cons
|
⊢ ∀ h t• cons h t = h ↦g t |
|
list
|
⊢ ∀ h t  • list [] = nil ∧ list (Cons h t) = cons h (list t)
|
|
head
tail
|
⊢ head = fst ∧ tail = snd |
|
nth
|
⊢ ∀ n l • nth 0 l = head l ∧ nth (n + 1) l = nth n (tail l)
|
