Tweak

spectec/src/il/print.ml

@@ -217,8 +217,10 @@ and string_of_prem prem =
   | RulePr (id, mixop, e) ->
     string_of_id id ^ ": " ^ string_of_mixop mixop ^ string_of_exp_args e
   | IfPr e -> "if " ^ string_of_exp e
-  | LetPr (e1, e2, xs) ->
-    "where " ^ string_of_exp e1 ^ " = " ^ string_of_exp e2 ^ " {" ^ (String.concat ", " xs) ^ "}"
+  | LetPr (e1, e2, ids) ->
+    let ids' = List.map (fun x -> x $ no_region) ids in
+    "where " ^ string_of_exp e1 ^ " = " ^ string_of_exp e2 ^
+    " {" ^ (String.concat ", " (List.map string_of_id ids')) ^ "}"
   | ElsePr -> "otherwise"
   | IterPr ({it = IterPr _; _} as prem', iter) ->
     string_of_prem prem' ^ string_of_iterexp iter

spectec/src/il/valid.ml

@@ -550,11 +550,11 @@ and valid_prem env prem =
     valid_expmix env mixop e (mixop, t) e.at
   | IfPr e ->
     valid_exp env e (BoolT $ e.at)
-  | LetPr (e1, e2, xs) ->
+  | LetPr (e1, e2, ids) ->
     let t = infer_exp env e2 in
     valid_exp ~side:`Lhs env e1 t;
     valid_exp env e2 t;
-    let target_ids = Free.({empty with varid = Set.of_list xs}) in
+    let target_ids = Free.{empty with varid = Set.of_list ids} in
     let free_ids = Free.(free_exp e1) in
     if not (Free.subset target_ids free_ids) then
       error prem.at ("target identifier(s) " ^

spectec/src/util/lib.ml

@@ -48,8 +48,6 @@ struct
       match flatten_opt xos with
       | Some xs -> Some (x::xs)
       | None -> None
-
-  let assoc_map f = List.map (fun (k, v) -> (k, f v))
 end
 
 module Char =

spectec/src/util/lib.mli

@@ -13,7 +13,6 @@ sig
   val nub : ('a -> 'a -> bool) -> 'a list -> 'a list
   val filter_not : ('a -> bool) -> 'a list -> 'a list
   val flatten_opt : 'a option list -> 'a list option
-  val assoc_map : ('a -> 'b) -> ('k * 'a) list -> ('k * 'b) list
 end
 
 module Char :