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: Oct 13 2024 at 01:02 UTC