Re-instate assignment order assertion

1 files changed, 2 insertions, 2 deletions

diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml
index 65e139c..af0d14b 100644
--- a/rego-proofs/compiler-rewrite/lib/compiler.ml
+++ b/rego-proofs/compiler-rewrite/lib/compiler.ml
@@ -283,8 +283,8 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function
      (* Call is a special case, being the only kind of "term" that affects scope. *)
      | Call ((Var "assign", []), [ Var name; rhs ]) ->
        (* Assumption: `name' is in the `env' because of our up-front variable analysis, but we've marked it as unassigned. *)
-       let { lean_id; kind; _ } = Map.find_exn env name in
-       (* assert (not assigned) ; *)
+       let { lean_id; kind; assigned } = Map.find_exn env name in
+       assert ((not assigned) || not (equal_definition_kind kind Complete)) ;
 
        let variable = { assigned = true; lean_id; kind } in
        let env' = Map.set env ~key:name ~data:variable in