From a0f1135d1a315b7bd876bb42cf80fc03645f4dae Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Sat, 19 Mar 2011 14:15:17 -0700 Subject: [PATCH] change LetRec rule to allow only a single expression in the body --- src/HaskProof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/HaskProof.v b/src/HaskProof.v index 2afb2de..e0cef35 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -109,7 +109,7 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l, Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]] [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]] -| RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ] +| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ] | RCase : forall Γ Δ lev tc Σ avars tbranches (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)), Rule -- 1.7.10.4