From d68d1e959091b186ebb5cbecf53992307b852f0d Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Sun, 25 Sep 2016 09:25:32 +0900
Subject: Catch formal type system up to reality, in progress

---
 language/l2_typ.ott | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'language/l2_typ.ott')

diff --git a/language/l2_typ.ott b/language/l2_typ.ott
index c4c6d0b2..43077d60 100644
--- a/language/l2_typ.ott
+++ b/language/l2_typ.ott
@@ -84,6 +84,7 @@ tag :: 'Tag_' ::=
 
 ne :: 'Ne_' ::=
  {{ com internal numeric expressions }}
+   | x                                   :: :: id
    | ' x                                 :: :: var
    | num                                 :: :: const
    | infinity                            :: :: inf
@@ -214,6 +215,20 @@ conformsto :: 'conformsto_' ::=
  | full :: :: full
  | parm :: :: parm
 
+widenvec :: 'widenvec_' ::=
+  | vectors :: :: widen
+  | none    :: :: dont
+  | _       :: :: dontcare
+
+widennum :: 'widennum_' ::=
+  | nums  :: :: widen
+  | none  :: :: dont
+  | _     :: :: dontcare
+
+widening :: 'widening_' ::=
+  {{ com Should we widen vector start locations, should we widen atoms and ranges }}
+  | ( widennum , widenvec ) :: :: w
+
  E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::=   {{ phantom }}
                                                                             {{ hol tid |-> tinf}}
                                                                             {{ lem map tid tinf }} 
-- 
cgit v1.2.3