Skip to content

Get rid of duplicated lemmas for commutative operations #315

Open
@hjorthjort

Description

@hjorthjort

KEVM uses the following lemmas to push symbolic values to the left in commutative-associative operations: https://github.com/kframework/evm-semantics/blob/master/tests/specs/lemmas.k#L290

We should add the same or similar lemmas, and go over our lemmas file and look for other cases where this can be simplified.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions