From 358d686692c40722885eaeffc7203e32142af7c8 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 14:15:14 -0700 Subject: [PATCH] add closedNDtoNormalND to NaturalDeduction --- src/NaturalDeduction.v | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/NaturalDeduction.v b/src/NaturalDeduction.v index f8baff0..2bc361f 100644 --- 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. -- 1.7.10.4