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?

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: Jun 15 2024 at 08:01 UTC