diff options
| author | Alasdair | 2018-12-12 03:42:10 +0000 |
|---|---|---|
| committer | Alasdair | 2018-12-12 03:42:10 +0000 |
| commit | ed5b58ba3a5a73253565edcb6460d2b48f56f887 (patch) | |
| tree | 573c358d079adcc59a7eb767857ec3119d3a646e /language | |
| parent | cdf287dfb69275e479d79ebc0d305e365dd3ee7b (diff) | |
Generalise existentials for non-integer type variables
Diffstat (limited to 'language')
| -rw-r--r-- | language/sail.ott | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/sail.ott b/language/sail.ott index 75527cc9..063b4cb9 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -234,9 +234,10 @@ typ :: 'Typ_' ::= | ( typ1 , ... , typn ) -> typ2 effectkw effect :: :: fn {{ com Function (first-order only) }} | typ1 <-> typ2 :: :: bidir {{ com Mapping }} | ( typ1 , .... , typn ) :: :: tup {{ com Tuple }} - | { kid1 ... kidn , n_constraint . typ } :: :: exist | id ( typ_arg1 , ... , typ_argn ) :: :: app {{ com type constructor application }} | ( typ ) :: S :: paren {{ ichlo [[typ]] }} + | { kinded_id1 ... kinded_idn , n_constraint . typ } + :: :: exist typ_arg :: 'A_' ::= {{ com type constructor arguments of all kinds }} |