Skip to content
Snippets Groups Projects
Commit 14ccc4c8 authored by Ralf Jung's avatar Ralf Jung
Browse files

add compute_by

parent c85d0f7a
No related branches found
No related tags found
1 merge request!261add tactic for solving computable goals
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 2 deletions
theories/decidable.v
+ 5
− 2
View file @ 14ccc4c8
...@@ -139,12 +139,15 @@ Proof. apply bool_decide_eq_false. Qed. ...@@ -139,12 +139,15 @@ Proof. apply bool_decide_eq_false. Qed.
- Goals `P` where `Decidable P` can be derived. - Goals `P` where `Decidable P` can be derived.
- Goals that compute to `True` or `x = x`. - Goals that compute to `True` or `x = x`.
The goal is solved by using `vm_compute` and then using a trivial proof term The goal must be a ground term for this, i.e., not contain variables (that do
(`I`/`eq_refl`). *) not compute away). The goal is solved by using `vm_compute` and then using a
trivial proof term (`I`/`eq_refl`). *)
Tactic Notation "compute_done" := Tactic Notation "compute_done" :=
try apply (bool_decide_unpack _); try apply (bool_decide_unpack _);
vm_compute; vm_compute;
first [ exact I | exact eq_refl ]. first [ exact I | exact eq_refl ].
Tactic Notation "compute_by" tactic(tac) :=
tac; compute_done.
(** Backwards compatibility notations. *) (** Backwards compatibility notations. *)
Notation bool_decide_true := bool_decide_eq_true_2. Notation bool_decide_true := bool_decide_eq_true_2.
......
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