Require Import Preamble.
Require Import General.
Require Import NaturalDeduction.
-Require Import NaturalDeductionToLatex.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import HaskKinds.
Instance ToLatexMathJudgment : ToLatexMath Judg :=
{ toLatexMath := judgmentToRawLatexMath }.
-Fixpoint nd_uruleToRawLatexMath {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string :=
+Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string :=
match r with
| RLeft _ _ _ r => nd_uruleToRawLatexMath r
| RRight _ _ _ r => nd_uruleToRawLatexMath r
- | RCanL _ _ => "CanL"
- | RCanR _ _ => "CanR"
- | RuCanL _ _ => "uCanL"
- | RuCanR _ _ => "uCanR"
- | RAssoc _ _ _ _ => "Assoc"
- | RCossa _ _ _ _ => "Cossa"
- | RExch _ _ _ => "Exch"
- | RWeak _ _ => "Weak"
- | RCont _ _ => "Cont"
+ | RCanL _ => "CanL"
+ | RCanR _ => "CanR"
+ | RuCanL _ => "uCanL"
+ | RuCanR _ => "uCanR"
+ | RAssoc _ _ _ => "Assoc"
+ | RCossa _ _ _ => "Cossa"
+ | RExch _ _ => "Exch"
+ | RWeak _ => "Weak"
+ | RCont _ => "Cont"
+ | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *)
end.
Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
match r with
- | RURule _ _ _ _ r => nd_uruleToRawLatexMath r
+ | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r
| RNote _ _ _ _ _ _ => "Note"
| RLit _ _ _ _ => "Lit"
| RVar _ _ _ _ => "Var"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RApp _ _ _ _ _ _ _ => "App"
| RLet _ _ _ _ _ _ _ => "Let"
- | RBindingGroup _ _ _ _ _ _ => "RBindingGroup"
+ | RJoin _ _ _ _ _ _ => "RJoin"
| RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
| REsc _ _ _ _ _ _ => "Esc"
- | REmptyGroup _ _ => "REmptyGroup"
+ | RVoid _ _ => "RVoid"
end.
-Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool :=
+Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
match r with
- | RLeft _ _ _ r => nd_hideURule r
- | RRight _ _ _ r => nd_hideURule r
- | RCanL _ _ => true
- | RCanR _ _ => true
- | RuCanL _ _ => true
- | RuCanR _ _ => true
- | RAssoc _ _ _ _ => true
- | RCossa _ _ _ _ => true
- | RExch _ (T_Leaf None) b => true
- | RExch _ a (T_Leaf None) => true
- | RWeak _ (T_Leaf None) => true
- | RCont _ (T_Leaf None) => true
- | _ => false
+ | RLeft _ _ _ r => nd_hideURule r
+ | RRight _ _ _ r => nd_hideURule r
+ | RCanL _ => true
+ | RCanR _ => true
+ | RuCanL _ => true
+ | RuCanR _ => true
+ | RAssoc _ _ _ => true
+ | RCossa _ _ _ => true
+ | RExch (T_Leaf None) b => true
+ | RExch a (T_Leaf None) => true
+ | RWeak (T_Leaf None) => true
+ | RCont (T_Leaf None) => true
+ | RComp _ _ _ _ _ => false (* FIXME: do better *)
+ | _ => false
end.
Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
match r with
- | RURule _ _ _ _ r => nd_hideURule r
- | REmptyGroup _ _ => true
- | RBindingGroup _ _ _ _ _ _ => true
+ | RArrange _ _ _ _ _ r => nd_hideURule r
+ | RVoid _ _ => true
+ | RJoin _ _ _ _ _ _ => true
| _ => false
end.
{ toLatexMath := fun r => rawLatexMath (@nd_ruleToRawLatexMath h c r) }.
Definition nd_ml_toLatexMath {c}(pf:@ND _ Rule [] c) :=
-@SCND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
- (mkSCND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).
+@SIND_toLatexMath _ _ ToLatexMathJudgment ToLatexMathRule (@nd_hideRule) _ _
+ (mkSIND (systemfc_all_rules_one_conclusion) _ _ _ pf (scnd_weak [])).