diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 3b5b9675..5bc630e5 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -46,6 +46,8 @@ End Morphism. Definition build_ex {T:Type} (n:T) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & ArithFact (P x)} := existT _ n H. +Definition build_ex2 {T:Type} {T':T -> Type} (n:T) (m:T' n) {P:T -> Prop} `{H:ArithFact (P n)} : {x : T & T' x & ArithFact (P x)} := + existT2 _ _ n m H. Definition generic_eq {T:Type} (x y:T) `{Decidable (x = y)} := Decidable_witness. Definition generic_neq {T:Type} (x y:T) `{Decidable (x = y)} := negb Decidable_witness. |