Require Import HaskKinds.
Require Import HaskWeakVars.
Require Import HaskWeakTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskStrong.
Require Import HaskProof.
| nil => t''
| lv => (rawLatexMath " ")+++t''+++(rawLatexMath " @ ")+++
(fold_left (fun x y => x+++(rawLatexMath ":")+++y)
- (map (fun l:HaskTyVar Γ ★ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
+ (map (fun l:HaskTyVar Γ _ => l (fun _ => LatexMath) ite) lv) (rawLatexMath ""))
end
end); try apply ConcatenableLatexMath.
try apply VarNameMonad.
Definition judgmentToRawLatexMath (j:Judg) : LatexMath :=
match match j return VarNameStoreM LatexMath with
- | mkJudg Γ Δ Σ₁ Σ₂ =>
+ | mkJudg Γ Δ Σ₁ Σ₂ l =>
bind Σ₁' = treeM (mapOptionTree ltypeToLatexMath Σ₁)
- ; bind Σ₂' = treeM (mapOptionTree ltypeToLatexMath Σ₂)
+ ; bind Σ₂' = treeM (mapOptionTree (fun t => ltypeToLatexMath (t@@l)) Σ₂)
; return treeToLatexMath Σ₁' +++ (rawLatexMath "\vdash") +++ treeToLatexMath Σ₂'
end with
varNameStoreM f => fst (f (varNameStore 0 0 0))
match r with
| RLeft _ _ _ r => nd_uruleToRawLatexMath r
| RRight _ _ _ r => nd_uruleToRawLatexMath r
+ | RId _ => "Id"
| RCanL _ => "CanL"
| RCanR _ => "CanR"
| RuCanL _ => "uCanL"
Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string :=
match r with
- | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r
+ | RArrange _ _ _ _ _ _ r => nd_uruleToRawLatexMath r
| RNote _ _ _ _ _ _ => "Note"
| RLit _ _ _ _ => "Lit"
| RVar _ _ _ _ => "Var"
| RAbsCo _ _ _ _ _ _ _ _ => "AbsCo"
| RApp _ _ _ _ _ _ _ => "App"
| RLet _ _ _ _ _ _ _ => "Let"
- | RJoin _ _ _ _ _ _ => "RJoin"
+ | RWhere _ _ _ _ _ _ _ _ => "Where"
+ | RJoin _ _ _ _ _ _ _ => "RJoin"
| RLetRec _ _ _ _ _ _ => "LetRec"
| RCase _ _ _ _ _ _ _ _ => "Case"
| RBrak _ _ _ _ _ _ => "Brak"
| REsc _ _ _ _ _ _ => "Esc"
- | RVoid _ _ => "RVoid"
+ | RVoid _ _ _ => "RVoid"
end.
Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool :=
end.
Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool :=
match r with
- | RArrange _ _ _ _ _ r => nd_hideURule r
- | RVoid _ _ => true
- | RJoin _ _ _ _ _ _ => true
+ | RArrange _ _ _ _ _ _ r => nd_hideURule r
+ | RVoid _ _ _ => true
+ | RJoin _ _ _ _ _ _ _ => true
| _ => false
end.