diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-16 13:36:10 -0400 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2013-08-16 13:36:10 -0400 |
| commit | ac382ab999dfcc612550f0ea95e750fe44ba4a9d (patch) | |
| tree | f550d6b25f1ba2a7a1da27dcf673343627bbb521 /docs/core-spec | |
| parent | 82d5aa03834b7368967d7a69901f9c0290f2e51c (diff) | |
| download | haskell-ac382ab999dfcc612550f0ea95e750fe44ba4a9d.tar.gz | |
Fix Trac #8138.
The code in CoreLint did not take into account the possibility of
~R# arguments to functions. These can arise in argToPat in SpecConstr.
Now, CoreLint does not fail when it sees a ~R# parameter.
This commit also updates the core-spec document accordingly.
Diffstat (limited to 'docs/core-spec')
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 6 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 359837 -> 335916 bytes |
2 files changed, 5 insertions, 1 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index c2dba49612..f2799841dc 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -122,9 +122,13 @@ G |-ty t : k2 G |-tm case e as z_s return t of </ alti // i /> : t G |-co g : t1 ~Nom k t2 --------------------- :: Coercion +-------------------- :: CoercionNom G |-tm g : t1 ~#k t2 +G |-co g : t1 ~Rep k t2 +----------------------- :: CoercionRep +G |-tm g : (~R#) k t1 t2 + defn G |- name n ok :: :: lintSingleBinding_lintBinder :: 'Name_' {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }} {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }} diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex cb21286abb..4e4ca924fb 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |