diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2015-04-23 16:02:43 -0400 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2015-04-24 17:00:25 -0400 |
| commit | 414e20bc7f5166d020ace3d92cd605e121d5eb3c (patch) | |
| tree | 7c2fa39eed6543cf449279625b15f65e9c434df1 /docs/core-spec/CoreLint.ott | |
| parent | a8d39a7255df187b742fecc049f0de6528b9acad (diff) | |
| download | haskell-414e20bc7f5166d020ace3d92cd605e121d5eb3c.tar.gz | |
Fix the formal operational semantics (#10121)
This adapts the work of Christiaan Baaij to present a sensible
operational semantics for FC with mutual recursion.
Diffstat (limited to 'docs/core-spec/CoreLint.ott')
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 6015731257..7058e8a113 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -209,7 +209,7 @@ G |-co z_(s ~R#k t) : s ~Rep k t G |-ty t1 : k1 G |-ty t2 : k2 -R <= Phant \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2 +R <= Ph \/ not (k1 <: OpenKind) \/ not (k2 <: OpenKind) \/ compatibleUnBoxedTys t1 t2 ------------------------------------------------------------------------ :: UnivCo G |-co t1 ==>!_R t2 : t1 ~R k2 t2 @@ -276,7 +276,7 @@ G |-co mu </ ti // i /> </ gj // j /> : t'1 ~R' k0 t'2 defn validRoles T :: :: checkValidRoles :: 'Cvr_' {{ com Type constructor role validity, \coderef{typecheck/TcTyClsDecls.lhs}{checkValidRoles} }} -by +by </ Ki // i /> = tyConDataCons T </ Rj // j /> = tyConRoles T @@ -341,7 +341,7 @@ Nom <= R R <= Ph ------- :: Refl -R <= R +R <= R defn G |- ki k ok :: :: lintKind :: 'K_' {{ com Kind validity, \coderef{coreSyn/CoreLint.lhs}{lintKind} }} @@ -352,7 +352,7 @@ G |-ty k : BOX -------------- :: Box G |-ki k ok -defn G |- ty t : k :: :: lintType :: 'Ty_' +defn G |- ty t : k :: :: lintType :: 'Ty_' {{ com Kinding, \coderef{coreSyn/CoreLint.lhs}{lintType} }} {{ tex [[G]] \labeledjudge{ty} [[t]] : [[k]] }} by |