Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- Inductive Arrow (A B:Type) : Type :=
- | ar_intro : (forall a:A, B) -> Arrow A B.
- Inductive DepArrow (A:Type) (B:A->Type) : Type :=
- | ar_intro : (forall a:A, B a) -> DepArrow A B.
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
