Mercurial > cpdt > repo

comparison src/Extensional.v @ 257:108ec446fbaf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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