Minor tweaks

spectec/src/el/eq.mli

@@ -3,3 +3,5 @@ open Ast
 val eq_iter : iter -> iter -> bool
 val eq_exp : exp -> exp -> bool
 val eq_typ : typ -> typ -> bool
+
+val eq_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

spectec/src/frontend/elab.ml

@@ -768,11 +768,11 @@ and elab_exp_notation' env e t : Il.exp list =
   | (EpsE | SeqE _), IterT (t1, iter) ->
     [elab_exp_notation_iter env (unseq_exp e) (t1, iter) t e.at]
   | IterE (e1, iter1), IterT (t1, iter) ->
-    if (iter = Opt) && (iter1 <> Opt) then
+    if iter = Opt && iter1 <> Opt then
       error_typ e.at "iteration expression" t;
     let es1' = elab_exp_notation' env e1 t1 in
-    let iter1' = elab_iter env iter1 in
-    [Il.IterE (tup_exp' es1' e1.at, (iter1', [])) $$ e.at % !!!env t]
+    let iter1' = elab_iterexp env iter1 in
+    [Il.IterE (tup_exp' es1' e1.at, iter1') $$ e.at % !!!env t]
   (* Significant parentheses indicate a singleton *)
   | ParenE (e1, true), IterT (t1, iter) ->
     let es' = elab_exp_notation' env e1 t1 in

spectec/src/il/eq.mli

@@ -5,3 +5,6 @@ val eq_iter : iter -> iter -> bool
 val eq_typ : typ -> typ -> bool
 val eq_exp : exp -> exp -> bool
 val eq_prem : premise -> premise -> bool
+
+val eq_opt : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool
+val eq_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool

spectec/src/il/validation.ml

@@ -246,9 +246,7 @@ let rec valid_iter env iter =
     valid_exp env e (NatT $ e.at);
     let t', dim = find "variable" env.vars id in
     equiv_typ env t' (NatT $ e.at) e.at;
-    match dim with
-    | [ListN (e', None)] when Eq.eq_exp e e' -> ()
-    | _ ->
+    if not Eq.(eq_list eq_iter dim [ListN (e, None)]) then
       error e.at ("use of iterated variable `" ^
         id.it ^ String.concat "" (List.map string_of_iter dim) ^
         "` outside suitable iteraton context")