Stream: Coq users

Topic: User-customizable simpl?

view this post on Zulip Joshua Grosso (Aug 13 2021 at 22:32):

Is there a way to add lemmas to simpl, a la Lean's or Isabelle's simp?

view this post on Zulip Guillaume Claret (Aug 13 2021 at 22:52):

Would the autorewrite tactic help? https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:tacn.autorewrite

view this post on Zulip Paolo Giarrusso (Aug 13 2021 at 23:07):

Modulo performance, yes. I guess it's sometimes acceptable — after all, it works (slowly) for autosubst 1

Last updated: Oct 03 2023 at 04:02 UTC