The Theory gst-lists
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
fill• list [] = nil ∧ list (Cons h t) = cons h (list t)
head
tail
⊢ head = fst ∧ tail = snd
nth
⊢ ∀ n l
fill• nth 0 l = head l ∧ nth (n + 1) l = nth n (tail l)

up quick index

privacy policy

Created:

V