diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-11-07 01:50:38 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-11-07 01:50:38 -0500 |
| commit | 5e3210fe6cca5dfdfee8483fea89f6d16d6f3d05 (patch) | |
| tree | 9a61c5d12b141385e0f6e18ebfeefd6e0d778006 | |
| parent | 538a0b6a0c61458133d146d79834fde4d2364546 (diff) | |
Add SideConditionFramework
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Specific/Framework/SideConditionFramework.v | 13 |
2 files changed, 14 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index a3b0846bd..fecae0fc5 100644 --- a/_CoqProject +++ b/_CoqProject @@ -272,6 +272,7 @@ src/Specific/Framework/Packages.v src/Specific/Framework/RawCurveParameters.v src/Specific/Framework/ReificationTypes.v src/Specific/Framework/ReificationTypesPackage.v +src/Specific/Framework/SideConditionFramework.v src/Specific/Framework/SynthesisFramework.v src/Specific/Framework/ArithmeticSynthesis/Base.v src/Specific/Framework/ArithmeticSynthesis/BasePackage.v diff --git a/src/Specific/Framework/SideConditionFramework.v b/src/Specific/Framework/SideConditionFramework.v new file mode 100644 index 000000000..51322b129 --- /dev/null +++ b/src/Specific/Framework/SideConditionFramework.v @@ -0,0 +1,13 @@ +Require Import Crypto.Util.Decidable. + +Definition vm_decide_package (P : Prop) := P. +Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P. +Definition vm_compute_reflexivity_package (P : Prop) := P. + +Ltac autosolve else_tac := + lazymatch goal with + | [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide + | [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide + | [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity + | _ => else_tac () + end. |