Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- data ℕ : Set where -- Don't let the word "Set" mislead you. "Type" would be a better name.
- Z : ℕ
- S : ℕ → ℕ
- data Fin : ℕ → Set where
- FZ : {n : ℕ} → Fin (S n)
- FS : {n : ℕ} → Fin n → Fin (S n)
Add Comment
Please, Sign In to add comment
