projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
90316bd
)
add closedNDtoNormalND to NaturalDeduction
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:14 +0000
(14:15 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:14 +0000
(14:15 -0700)
src/NaturalDeduction.v
patch
|
blob
|
history
diff --git
a/src/NaturalDeduction.v
b/src/NaturalDeduction.v
index
f8baff0
..
2bc361f
100644
(file)
--- a/
src/NaturalDeduction.v
+++ b/
src/NaturalDeduction.v
@@
-299,6
+299,14
@@
Section Natural_Deduction.
apply q2. subst. apply cnd0.
Defined.
+ (* undo the above *)
+ Fixpoint closedNDtoNormalND {c}(cnd:ClosedND c) : ND [] c :=
+ match cnd in ClosedND C return ND [] C with
+ | cnd_weak => nd_id0
+ | cnd_rule h c cndh rhc => closedNDtoNormalND cndh ;; nd_rule rhc
+ | cnd_branch c1 c2 cnd1 cnd2 => nd_llecnac ;; nd_prod (closedNDtoNormalND cnd1) (closedNDtoNormalND cnd2)
+ end.
+
Close Scope nd_scope.
Open Scope pf_scope.