diff options
Diffstat (limited to 'docs/core-spec')
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 4 | ||||
| -rw-r--r-- | docs/core-spec/CoreSyn.ott | 6 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.mng | 2 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 354307 -> 355707 bytes |
4 files changed, 7 insertions, 5 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index 3a3468d53b..d18525a028 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -300,11 +300,11 @@ not (si is_a_coercion) not (ti is_a_coercion) R' = (tyConRolesX R T)[i] ---------------------- :: NthCoTyCon -G |-co nth i g : si k2~R' 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 0 g : k1 *~Nom * k2 +G |-co nth Nom 0 g : k1 *~Nom * k2 G |-co g : (s1 s2) k~Nom k' (t1 t2) G |-ty s1 : k1 diff --git a/docs/core-spec/CoreSyn.ott b/docs/core-spec/CoreSyn.ott index 78118d532c..e12f68ba4f 100644 --- a/docs/core-spec/CoreSyn.ott +++ b/docs/core-spec/CoreSyn.ott @@ -152,8 +152,8 @@ g {{ tex \gamma }}, h {{ tex \eta }} :: 'Coercion_' ::= {{ com Coercions, \coder | g1 ; g2 :: :: TransCo {{ com \ctor{TransCo}: Transitivity }} | mu </ ti // i /> $ </ gj // j /> :: :: AxiomRuleCo {{ com \ctor{AxiomRuleCo}: Axiom-rule application (for type-nats) }} - | nth I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }} - {{ tex \textsf{nth}^{[[I]]}\,[[g]] }} + | nth R I g :: :: NthCo {{ com \ctor{NthCo}: Projection (0-indexed) }} + {{ tex \textsf{nth}^{[[I]]}_{[[R]]}\,[[g]] }} | LorR g :: :: LRCo {{ com \ctor{LRCo}: Left/right projection }} | g @ h :: :: InstCo {{ com \ctor{InstCo}: Instantiation }} | g |> h :: :: CoherenceCo {{ com \ctor{CoherenceCo}: Coherence }} @@ -453,6 +453,8 @@ formula :: 'formula_' ::= | role_list1 = role_list2 :: :: eq_role_list | R1 /= R2 :: :: role_neq | R1 = R2 :: :: eq_role + | R1 <= R2 :: :: lte_role + {{ tex [[R1]] \leq [[R2]] }} | </ Ki // i /> = tyConDataCons T :: :: tyConDataCons | O ( n ) = R :: :: role_lookup | R elt role_list :: :: role_elt diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng index 580032129d..64e90bb7d0 100644 --- a/docs/core-spec/core-spec.mng +++ b/docs/core-spec/core-spec.mng @@ -30,7 +30,7 @@ System FC, as implemented in GHC\footnote{This document was originally prepared by Richard Eisenberg (\texttt{eir@cis.upenn.edu}), but it should be maintained by anyone who edits the functions or data structures mentioned in this file. Please feel free to contact Richard for more information.}\\ -\Large 23 October, 2015 +\Large 26 January, 2018 \end{center} \section{Introduction} diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex 1e139115cd..3732818e2e 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |