Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive array (T:Type) : nat -> Type :=
- | ar_empty : array T 0
- | ar_ext : forall n, T -> array T n -> array T (S n).
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
