https://github.com/c-corn/corn
Tip revision: af4b86e6ad6cfd242562f9c33c0e438298fc4e1f authored by Théo Zimmermann on 07 September 2021, 14:21:48 UTC
Merge pull request #161 from Zimmi48/update-ci-8.13
Merge pull request #161 from Zimmi48/update-ci-8.13
Tip revision: af4b86e
Ranges.v
Require Import Program MathClasses.interfaces.canonical_names util.Container QArith QMinMax CRlattice.
Definition Range (T: Type) := prod T T.
Instance in_QRange: Container Q (Range Q)
:= λ r x, (Qmin (fst r) (snd r) <= x <= Qmax (fst r) (snd r))%Q.
Instance in_CRRange: Container (msp_car CR) (Range (msp_car CR))
:= λ r x,
(ucFun (ucFun CRmin (fst r)) (snd r) <= x)%CR
∧ (x <= ucFun (ucFun CRmax (fst r)) (snd r))%CR.
Instance in_sig_Range `{Container A (Range A)} (P: A → Prop): Container (sig P) (Range (sig P))
:= λ r x, In (` (fst r), ` (snd r)) (` x).