Skip to content

Commit

Permalink
Remove unused variable
Browse files Browse the repository at this point in the history
  • Loading branch information
virgil-serbanuta committed Oct 7, 2023
1 parent b790832 commit 4497c78
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 5 deletions.
4 changes: 1 addition & 3 deletions kmxwasm/src/kmxwasm/lemmas/expression.py
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,4 @@ def mandos_cell(*args: KInner) -> KApply:


def proofOperationList(proof: Iterable[KInner]) -> KInner: # noqa: N802
return simple_list(
concat_label='proofOperationList', empty_label='.List{"proofOperationList"}', items=proof
)
return simple_list(concat_label='proofOperationList', empty_label='.List{"proofOperationList"}', items=proof)
2 changes: 0 additions & 2 deletions kmxwasm/src/kmxwasm/lemmas/lemmas.py
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,6 @@ def make_rule(self, kast_defn: KDefinition) -> KRule:
rhs_vars = free_vars(self.rhs)
var_occurrences = count_vars(mlAnd([KRewrite(self.lhs, self.rhs), self.requires]))
v_subst: dict[str, KVariable] = {}
vremap_subst: dict[str, KVariable] = {}
for v in var_occurrences:
new_v = v
if var_occurrences[v] == 1:
Expand All @@ -65,7 +64,6 @@ def make_rule(self, kast_defn: KDefinition) -> KRule:
new_v = '?' + new_v
if new_v != v:
v_subst[v] = KVariable(new_v)
vremap_subst[new_v] = KVariable(v)

lhs = Subst(v_subst)(self.lhs)
rhs = self.rhs # apply_existential_substitutions(Subst(v_subst)(self.rhs))
Expand Down

0 comments on commit 4497c78

Please sign in to comment.