diff options
| author | Brian Campbell | 2018-06-01 16:06:05 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-08 15:03:37 +0100 |
| commit | 6b485cb062f474454b467c53edff69b10f6d3b5f (patch) | |
| tree | c86a352c9097912301a2c517e0bc74f353efdc34 /lib | |
| parent | ea2017301f3cb9d82883407ab1628956c4eb287d (diff) | |
Coq: some very basic existential support
Only single variable in places, only packed at literals and variables,
no unpacking
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail_values.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/coq/Sail_values.v b/lib/coq/Sail_values.v index 0dc25e1b..2343490b 100644 --- a/lib/coq/Sail_values.v +++ b/lib/coq/Sail_values.v @@ -19,6 +19,9 @@ Lemma use_ArithFact {P} `(ArithFact P) : P. apply fact. Defined. +Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} := + existT _ n H. + Definition ii := Z. Definition nn := nat. |