Stream: Coq users

Topic: is_evar tactic


view this post on Zulip Théo Zimmermann (Nov 18 2022 at 14:42):

Is it normal / expected that I need the ? for this to succeed? If I remove it, it fails with "Not evar". I wonder what's the use case for this tactic if this behavior is expected.

Goal True.
evar (P: Prop).
is_evar P.

Last updated: Feb 09 2023 at 00:03 UTC