diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 4 |
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 |