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) |