Skip to content

Tracking issue for slow field_simp calls replaced by simp #15486

@grunweg

Description

@grunweg

The field_simp tactic can be really useful, but can also be really slow: its implementation is in need of a rewrite.

Until that has happened, some really slow field_simp calls were replaced by simp calls:
field_simp [x, y] is equivalent to simp ...; usually, this replacement itself does not provide a large speed-up, but squeezing the simp call does. (Squeezing the field_simp, i.e. replacing by the output of field_simp?, did not help much.)
This issue tracks these replacements: after field_simp has been improved, these calls should be reinstated.

Metadata

Metadata

Assignees

No one assigned

    Labels

    t-metaTactics, attributes or user commands

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions