diff --git a/haskell.mng b/haskell.mng index 26036b7084c5bdf1d18d93b9a31be3cf895cf987..f3b13f1513eb79c337c8d82c9b3ed96f724af137 100644 --- a/haskell.mng +++ b/haskell.mng @@ -100,6 +100,7 @@ wish to do this, though, so the rule is not included. Note the convention in thi document of rendering rejected rules with a ``XX'' prefix and suffix. \end{aside} +\drules[FE]{$[[G |-FE funeq -| f ; s]]$}{Function equations}{Fun} \drules[FL]{$[[G |-FL funlhs : ts -| G'; f; s]]$}{Function left-hand sides}{Std,ResSig} The \ent{FL} judgment checks a function left-hand side. In the standard case (\rref{FL-Std}), it checks diff --git a/rules.ott b/rules.ott index 8a970fa330766098d66d0462c4abb34b02d6f83b..5aaf01f023a9bd26a3a8d2413bebab3fbecc26c2 100644 --- a/rules.ott +++ b/rules.ott @@ -36,13 +36,13 @@ G |-FE funeq -| f ; s :: :: FunEq :: 'FE_' {{ com Function equation typing }} by G |-FL funlhs : ts -| G'; f; forall cs. Q => u -G', <c : type>, Q |- e : u +G', <c : type>, Q |-E e : u --------------------------------------------- :: Fun G |-FE funlhs = e -| f; forall cs. Q => ts -> u defn G |-FL funlhs : ts -| G' ; f ; s :: :: FunLhs :: 'FL_' {{ com Function left-hand side typing }} - {{ tex [[G]] \ent{FL} [[funlhs]] : [[ts]] [[-|]] ([[G']]; [[f]]; [[s]]) }} + {{ tex [[G]] \ent{FL} [[funlhs]] : [[ts]] [[-|]] [[G']]; [[f]]; [[s]] }} by G |-PS </ pi : ti // i /> -| G'