Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data ListOfSize (n:nat)
- empty : ListOfSize 0
- cons : (m:nat) -> (elt:bool) -> ListOfSize m -> ListOfSize (S m)
- tail : (n:Nat) -> (ls: ListOfSize (n + 1)) -> ListOfSize n
- case ls of
- cons _ _ ls1 -> ls1
Add Comment
Please, Sign In to add comment
