From fc3e8057ee3c7a03e8c3ad764ea348a241d540fc Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Fri, 25 Mar 2011 11:16:00 -0700 Subject: [PATCH] add LetRec case to Rule_Flat --- src/HaskProof.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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) -- 1.7.10.4