Mercurial > cpdt > repo
comparison 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 |
comparison
equal
deleted
inserted
replaced
256:4293dd6912cd | 257:108ec446fbaf |
---|---|
83 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. | 83 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. |
84 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. | 84 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope. |
85 | 85 |
86 Bind Scope source_scope with exp. | 86 Bind Scope source_scope with exp. |
87 | 87 |
88 Definition zero : Exp Nat := fun _ => ^0. | 88 Example zero : Exp Nat := fun _ => ^0. |
89 Definition one : Exp Nat := fun _ => ^1. | 89 Example one : Exp Nat := fun _ => ^1. |
90 Definition zpo : Exp Nat := fun _ => zero _ +^ one _. | 90 Example zpo : Exp Nat := fun _ => zero _ +^ one _. |
91 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x. | 91 Example ident : Exp (Nat --> Nat) := fun _ => \x, #x. |
92 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _. | 92 Example app_ident : Exp Nat := fun _ => ident _ @ zpo _. |
93 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => | 93 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => |
94 \f, \x, #f @ #x. | 94 \f, \x, #f @ #x. |
95 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. | 95 Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _. |
96 | 96 |
97 Fixpoint typeDenote (t : type) : Set := | 97 Fixpoint typeDenote (t : type) : Set := |
98 match t with | 98 match t with |
99 | Nat => nat | 99 | Nat => nat |
100 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | 100 | t1 --> t2 => typeDenote t1 -> typeDenote t2 |