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: Feb 04 2023 at 21:02 UTC