diff --git a/README.md b/README.md index 9b7c918f..b098582d 100644 --- a/README.md +++ b/README.md @@ -172,6 +172,7 @@ D ::= ... X A1 ... An = E ~> X : A1 -> ... -> An -> (= E) type X A1 ... An ~> X : A1 => ... => An => type type X A1 ... An = T ~> X : A1 => ... => An => (= type T) + X ~> X : (= X) (expressions) E ::= ... diff --git a/parser.mly b/parser.mly index 2b1930d3..1a0e59e3 100644 --- a/parser.mly +++ b/parser.mly @@ -183,6 +183,8 @@ atdec : | head typparamlist EQUAL exp { VarD($1, funT($2, EqT($4)@@ati 4, Pure@@ati 3)@@span[ati 2; ati 4]) @@at() } + | name + { VarD($1, funT([], EqT(VarE($1)@@ati 1)@@ati 1, Pure@@ati 1)@@ati 1)@@at() } | TYPE head typparamlist EQUAL typ { VarD($2, funT($3, EqT(TypE($5)@@ati 5)@@ati 5, Pure@@ati 4)@@at()) @@at() } diff --git a/regression.1ml b/regression.1ml index f798fb80..7a2f6ea7 100644 --- a/regression.1ml +++ b/regression.1ml @@ -2,6 +2,10 @@ record_inference x = x.works_a_little; ;; +type DEC_PUNNING = {int; list}; + +;; + Equivalence: { type t a b;