Library Mtac2.lib.Datatypes
Set Implicit Arguments.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Require Import Notations.
Inductive munit : Set :=
mtt : munit.
option A is the extension of A with an extra element None
Cumulative Inductive moption (A:Type) : Type :=
| mSome : A -> moption A
| mNone : moption A.
Arguments mSome {A} a.
Arguments mNone {A}.
Definition moption_map (A B:Type) (f:A->B) (o : moption A) : moption B :=
match o with
| mSome a => @mSome B (f a)
| mNone => @mNone B
end.
Inductive mprod (A B:Type) : Type :=
mpair : A -> B -> mprod A B.
Module ProdNotations.
Infix "*m" := (mprod) (at level 40) : type_scope.
Notation "(m: x , y , .. , z )" := (mpair .. (mpair x y) .. z) : core_scope.
Notation "(m: x ; .. ; y ; z )" := (mpair x .. (mpair y z) ..) : core_scope.
End ProdNotations.
Arguments mpair {A B} _ _.
Section projections.
Import ProdNotations.
Context {A : Type} {B : Type}.
Definition mfst (p:A *m B) := match p with
| (m: x, y) => x
end.
Definition msnd (p:A *m B) := match p with
| (m: x, y) => y
end.
End projections.
Polymorphic lists and some operations
Cumulative Inductive mlist (A : Type) : Type :=
| mnil : mlist A
| mcons : A -> mlist A -> mlist A.
Arguments mnil {A}.
Arguments mcons {A} a l.
Infix ":m:" := mcons (at level 60, right associativity) : mlist_scope.
Delimit Scope mlist_scope with mlist.
Bind Scope mlist_scope with mlist.
Local Open Scope mlist_scope.
Definition mlength (A : Type) : mlist A -> nat :=
fix length l :=
match l with
| mnil => O
| _ :m: l' => S (length l')
end.
Concatenation of two lists