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

Add test.

parent 92c79d91
No related branches found
No related tags found
1 merge request!434Use high cost for `Decision` instances for `True` and `False`.
Pipeline #75539 passed
The command has indeed failed with message:
No applicable tactic.
From stdpp Require Import list.
(** Test that Coq does not infer [x ∈ xs] as [False] by eagerly using
[False_dec] on a goal with unresolved type class instances. *)
Example issue_165 (x : nat) :
¬ xs : list nat, (guard (x xs); Some x) None.
Proof.
intros [xs Hxs]. case_option_guard; [|done].
Fail done. (* Would succeed if the instance backing [x ∈ xs] is infered as
[False]. *)
Abort.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment