Skip to content

Instantly share code, notes, and snippets.

@risou

risou/coqt1

Created April 6, 2011 03:24
Show Gist options
  • Save risou/905075 to your computer and use it in GitHub Desktop.
Save risou/905075 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coqt1
Definition plus (n : nat)(m : nat) : nat := n + m.
Definition id (A : Type)(x : A) : A := x.
Definition prop0 : forall (A : Prop), A -> A := fun A x => x.
Definition prop1 : forall (A B C : Prop), (B -> C) -> (A -> B) -> (A -> C) := fun A B C f g x => f (g x).
Definition q0 : forall (A B : Prop), A -> (A -> B) -> B := fun A B f g => g (f).
Definition q1 : forall (A B C : Prop), (A -> B -> C) -> (B -> A -> C) := fun A B C f x y => f y (x).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment