Stream: Coq users

Topic: Multimatch in auto

view this post on Zulip Patrick Nicodemus (Oct 30 2022 at 15:32):

Does multimatch display the same backtracking behavior if it's called from a Hint Extern in auto? Like if auto calls that Hint Extern, succeeds, moves on and then backtracks, will calling the same Hint Extern give the same result or a different one?

view this post on Zulip Jason Gross (Nov 01 2022 at 00:58):

Not in auto nor eauto. It might work the way you want it to in typeclasses eauto with core; try it?

Last updated: Oct 13 2024 at 01:02 UTC