projects
/
coq-hetmet.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
7b2698b
)
change LetRec rule to allow only a single expression in the body
author
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:17 +0000
(14:15 -0700)
committer
Adam Megacz
<megacz@cs.berkeley.edu>
Sat, 19 Mar 2011 21:15:17 +0000
(14:15 -0700)
src/HaskProof.v
patch
|
blob
|
history
diff --git
a/src/HaskProof.v
b/src/HaskProof.v
index
2afb2de
..
e0cef35
100644
(file)
--- a/
src/HaskProof.v
+++ b/
src/HaskProof.v
@@
-109,7
+109,7
@@
HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
[Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
| 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
| RCase : forall Γ Δ lev tc Σ avars tbranches
(alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
Rule