diff options
Diffstat (limited to 'docs/core-spec/CoreLint.ott')
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 1fb9e09559..d18525a028 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -299,13 +299,12 @@ G |-ty ti : k2' not (si is_a_coercion) not (ti is_a_coercion) R' = (tyConRolesX R T)[i] -R' <= R0 ---------------------- :: NthCoTyCon -G |-co nth R0 i g : si k2~R0 k2' ti +G |-co nth R' i g : si k2~R' k2' ti G |-co g : (forall z1_k1.t1) k3~R k4 (forall z2_k2.t2) --------------------------- :: NthCoForAll -G |-co nth R0 0 g : k1 *~R0 * k2 +G |-co nth Nom 0 g : k1 *~Nom * k2 G |-co g : (s1 s2) k~Nom k' (t1 t2) G |-ty s1 : k1 |