From: Adam Megacz Date: Fri, 25 Mar 2011 18:16:00 +0000 (-0700) Subject: add LetRec case to Rule_Flat X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=fc3e8057ee3c7a03e8c3ad764ea348a241d540fc add LetRec case to Rule_Flat --- diff --git a/src/HaskProof.v b/src/HaskProof.v index 55b0b03..ef669ee 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -133,7 +133,8 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l) | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l) | Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e) -| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x). +| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) +| Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). (* given a proof that uses only uniform rules, we can produce a general proof *) Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)