diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-07 15:08:26 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-07 15:08:26 -0500 |
commit | ae96b60dc9264703ed6a43c48e0c4892bffad131 (patch) | |
tree | da67980206c804a350133f1423e4535e672e4d52 /src/Util/SideConditions/CorePackages.v | |
parent | f92069a3ddddf551ac313d58dcf02abeb098069e (diff) |
Remove function evar package in favor of generic rel one
Diffstat (limited to 'src/Util/SideConditions/CorePackages.v')
-rw-r--r-- | src/Util/SideConditions/CorePackages.v | 27 |
1 files changed, 5 insertions, 22 deletions
diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v index 8126c5280..c1041d040 100644 --- a/src/Util/SideConditions/CorePackages.v +++ b/src/Util/SideConditions/CorePackages.v @@ -6,11 +6,11 @@ Record evar_package {T} (v : T) := Arguments val {T v} _. Arguments evar_package_pf {T v} _. -Record evar_function_package {A B} (f : forall x : A, B x) := - { valf : forall x : A, B x; - evarf_package_pf : forall x, valf x = f x }. -Arguments valf {A B f} _. -Arguments evarf_package_pf {A B f} _ _. +Record evar_rel_package {A} (f : A) B (R : B -> A -> Prop) := + { valr : B; + evarr_package_pf : R valr f }. +Arguments valr {A f B R} _. +Arguments evarr_package_pf {A f B R} _. Record evard_package {s d} (v : s) := { vald : d; @@ -20,21 +20,4 @@ Arguments vald {s d v} _. Arguments evard_package_pfT {s d v} _. Arguments evard_package_pf {s d v} _. -Local Notation "'rew' 'dependent' H 'in' H'" - := (match H with - | eq_refl => H' - end) - (at level 10, H' at level 10, - format "'[' 'rew' 'dependent' '/ ' H in '/' H' ']'"). - -Record evard_function_package {sA sB dA dB} (f : forall x : sA, sB x) := - { valdf : forall x : dA, dB x; - evardf_package_pfTA : dA = sA; - evardf_package_pfTB : forall x, sB (rew evardf_package_pfTA in x) = dB x; - evardf_package_pf : forall x, valdf x = rew dependent evardf_package_pfTB x in (f (rew evardf_package_pfTA in x)) }. -Arguments valdf {sA sB dA dB f} _ _. -Arguments evardf_package_pfTA {sA sB dA dB f} _. -Arguments evardf_package_pfTB {sA sB dA dB f} _. -Arguments evardf_package_pf {sA sB dA dB f} _ _. - Ltac autosolve else_tac := else_tac (). |