Skip to content
Snippets Groups Projects
Commit b81fb0fc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Do not call `done` recursively when solving `is_Some`.

parent 715cb884
No related branches found
No related tags found
1 merge request!296Do not call `done` recursively when solving `is_Some`.
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/option.v
+ 1
− 1
View file @ b81fb0fc
...@@ -40,7 +40,7 @@ Proof. congruence. Qed. ...@@ -40,7 +40,7 @@ Proof. congruence. Qed.
Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x. Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
Global Instance: Params (@is_Some) 1 := {}. Global Instance: Params (@is_Some) 1 := {}.
Global Hint Extern 0 (is_Some _) => by eexists : core. Global Hint Extern 0 (is_Some _) => eexists; reflexivity : core.
Lemma is_Some_alt {A} (mx : option A) : Lemma is_Some_alt {A} (mx : option A) :
is_Some mx ↔ match mx with Some _ => True | None => False end. is_Some mx ↔ match mx with Some _ => True | None => False end.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment