diff options
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 |