Mercurial > cpdt > repo
diff src/Extensional.v @ 257:108ec446fbaf
Easy direction of Intensional
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Wed, 16 Dec 2009 15:54:50 -0500 |
parents | 4293dd6912cd |
children | 2c88fc1dbe33 |
line wrap: on
line diff
--- a/src/Extensional.v Wed Dec 16 15:31:54 2009 -0500 +++ b/src/Extensional.v Wed Dec 16 15:54:50 2009 -0500 @@ -85,14 +85,14 @@ Bind Scope source_scope with exp. - Definition zero : Exp Nat := fun _ => ^0. - Definition one : Exp Nat := fun _ => ^1. - Definition zpo : Exp Nat := fun _ => zero _ +^ one _. - Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. - Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. - Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => + Example zero : Exp Nat := fun _ => ^0. + Example one : Exp Nat := fun _ => ^1. + Example zpo : Exp Nat := fun _ => zero _ +^ one _. + Example ident : Exp (Nat --> Nat) := fun _ => \x, #x. + Example app_ident : Exp Nat := fun _ => ident _ @ zpo _. + Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => \f, \x, #f @ #x. - Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. + Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. Fixpoint typeDenote (t : type) : Set := match t with