Mercurial > cpdt > repo

comparison src/Extensional.v @ 221:54e8ecb5ec88

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Port Reflection
author Adam Chlipala <adamc@hcoop.net>
date Mon, 16 Nov 2009 11:09:47 -0500
parents d1464997078d
children 4b73ea13574d
comparison
equal deleted inserted replaced
220:15501145d696 221:54e8ecb5ec88
485 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. 485 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope.
486 486
487 Delimit Scope source_scope with source. 487 Delimit Scope source_scope with source.
488 Bind Scope source_scope with exp. 488 Bind Scope source_scope with exp.
489 489
490 Open Local Scope source_scope. 490 Local Open Scope source_scope.
491 491
492 Fixpoint typeDenote (t : type) : Set := 492 Fixpoint typeDenote (t : type) : Set :=
493 match t with 493 match t with
494 | Unit => unit 494 | Unit => unit
495 | t1 --> t2 => typeDenote t1 -> typeDenote t2 495 | t1 --> t2 => typeDenote t1 -> typeDenote t2
726 End choice_tree. 726 End choice_tree.
727 727
728 Implicit Arguments merge [var t result]. 728 Implicit Arguments merge [var t result].
729 729
730 Section elaborate. 730 Section elaborate.
731 Open Local Scope elab_scope. 731 Local Open Scope elab_scope.
732 732
733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} : 733 Fixpoint elaboratePat var t1 ts result (p : pat t1 ts) {struct p} :
734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result := 734 (hlist (exp var) ts -> result) -> result -> choice_tree var t1 result :=
735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result) 735 match p in (pat t1 ts) return ((hlist (exp var) ts -> result)
736 -> result -> choice_tree var t1 result) with 736 -> result -> choice_tree var t1 result) with