Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data DiffNat n m where
- data LeqView n m where
- type (<) n m = (n <? m) ~ 'True
- type (<?) n m = (n + 1) <=? m
- (%<?) :: SNat n -> SNat m -> SBool (n <? m)
- type (>) n m = (n >? m) ~ 'True
- type (>?) n m = m <? n
- (%>?) :: SNat n -> SNat m -> SBool (n >? m)
- type (>=) n m = (n >=? m) ~ 'True
- type (>=?) n m = m <=? n
- (%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
- type family FlipOrdering ord where ...
- type Min n m = MinAux (n <=? m) n m
- sMin :: SNat n -> SNat m -> SNat (Min n m)
- type Max n m = MaxAux (n >=? m) n m
- sMax :: SNat n -> SNat m -> SNat (Max n m)
- sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)
- coerceLeqL :: forall n m l. (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l)
- coerceLeqR :: forall n m l. SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m)
- sLeqCongL :: (a :~: b) -> SNat c -> (a <= c) :~: (b <= c)
- sLeqCongR :: SNat a -> (b :~: c) -> (a <= b) :~: (a <= c)
- sLeqCong :: (a :~: b) -> (c :~: d) -> (a <= c) :~: (b <= d)
- succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m)
- compareCongR :: SNat a -> (b :~: c) -> CmpNat a b :~: CmpNat a c
- leqToCmp :: SNat a -> SNat b -> IsTrue (a <=? b) -> Either (a :~: b) (CmpNat a b :~: 'LT)
- eqlCmpEQ :: SNat a -> SNat b -> (a :~: b) -> CmpNat a b :~: 'EQ
- eqToRefl :: SNat a -> SNat b -> (CmpNat a b :~: 'EQ) -> a :~: b
- flipCmpNat :: SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a
- ltToNeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> (a :~: b) -> Void
- leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> ((a :~: b) -> Void) -> CmpNat a b :~: 'LT
- succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT
- ltToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (a <=? b)
- gtToLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'GT) -> IsTrue (b <=? a)
- congFlipOrdering :: (a :~: b) -> FlipOrdering a :~: FlipOrdering b
- ltToSuccLeq :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> IsTrue (Succ a <=? b)
- cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT
- leqToGT :: SNat a -> SNat b -> IsTrue (Succ b <=? a) -> CmpNat a b :~: 'GT
- cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT)
- zeroNoLT :: SNat a -> (CmpNat a 0 :~: 'LT) -> Void
- ltRightPredSucc :: SNat a -> SNat b -> (CmpNat a b :~: 'LT) -> b :~: Succ (Pred b)
- cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m)
- ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT
- cmpSuccStepR :: forall n m. SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
- ltSuccLToLT :: SNat n -> SNat m -> (CmpNat (Succ n) m :~: 'LT) -> CmpNat n m :~: 'LT
- leqToLT :: SNat a -> SNat b -> IsTrue (Succ a <=? b) -> CmpNat a b :~: 'LT
- leqZero :: SNat n -> IsTrue (0 <=? n)
- leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m)
- fromLeqView :: LeqView n m -> IsTrue (n <=? m)
- leqViewRefl :: SNat n -> LeqView n n
- viewLeq :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m
- leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
- leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
- leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <=? m)
- leqRefl :: SNat n -> IsTrue (n <=? n)
- leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m)
- leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m)
- leqReflexive :: SNat n -> SNat m -> (n :~: m) -> IsTrue (n <=? m)
- leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l)
- leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m
- plusMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k))
- leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0
- plusMonotoneL :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l))
- plusMonotoneR :: SNat n -> SNat m -> SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l))
- plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m))
- plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m))
- plusCancelLeqR :: SNat n -> SNat m -> SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m)
- plusCancelLeqL :: SNat n -> SNat m -> SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l)
- succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void
- succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False
- succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void
- succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False
- notLeqToLeq :: forall n m. (n <=? m) ~ 'False => SNat n -> SNat m -> IsTrue (m <=? n)
- leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m)
- leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n
- geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m
- minComm :: SNat n -> SNat m -> Min n m :~: Min m n
- minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n)
- minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m)
- minLargest :: SNat l -> SNat n -> SNat m -> IsTrue (l <=? n) -> IsTrue (l <=? m) -> IsTrue (l <=? Min n m)
- leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m
- geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n
- maxComm :: SNat n -> SNat m -> Max n m :~: Max m n
- maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m)
- maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m)
- maxLeast :: SNat l -> SNat n -> SNat m -> IsTrue (n <=? l) -> IsTrue (m <=? l) -> IsTrue (Max n m <=? l)
- lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)
- lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)
- lneqToLT :: SNat n -> SNat m -> IsTrue (n <? m) -> CmpNat n m :~: 'LT
- ltToLneq :: SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> IsTrue (n <? m)
- lneqZero :: SNat a -> IsTrue (0 <? Succ a)
- lneqSucc :: SNat n -> IsTrue (n <? Succ n)
- succLneqSucc :: SNat n -> SNat m -> (n <? m) :~: (Succ n <? Succ m)
- lneqRightPredSucc :: SNat n -> SNat m -> IsTrue (n <? m) -> m :~: Succ (Pred m)
- lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <? m) -> IsTrue (n <? m)
- lneqSuccStepR :: SNat n -> SNat m -> IsTrue (n <? m) -> IsTrue (n <? Succ m)
- plusStrictMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <? m) -> IsTrue (l <? k) -> IsTrue ((n + l) <? (m + k))
- maxZeroL :: SNat n -> Max 0 n :~: n
- maxZeroR :: SNat n -> Max n 0 :~: n
- minZeroL :: SNat n -> Min 0 n :~: 0
- minZeroR :: SNat n -> Min n 0 :~: 0
- minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> (Succ n - m) :~: Succ (n - m)
- lneqZeroAbsurd :: SNat n -> IsTrue (n <? 0) -> Void
- minusPlus :: forall n m. SNat n -> SNat m -> IsTrue (m <=? n) -> ((n - m) + m) :~: n
- minPlusTruncMinus :: SNat n -> SNat m -> (Min n m + (n -. m)) :~: n
- truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n)
- type (-.) n m = Subt n m (m <=? n)
- (%-.) :: SNat n -> SNat m -> SNat (n -. m)
- type LeqWitness n m = IsTrue (n <=? m)
- data a :<: b
- data Leq n m where
- leqRhs :: Leq n m -> SNat m
- leqLhs :: Leq n m -> SNat n
- propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m
- boolToPropLeq :: n <= m => SNat n -> SNat m -> Leq n m
- propToBoolLt :: (n :<: m) -> IsTrue (n <? m)
- boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m
Documentation
type family FlipOrdering ord where ... Source #
FlipOrdering 'LT = 'GT | |
FlipOrdering 'GT = 'LT | |
FlipOrdering 'EQ = 'EQ |
Lemmas
sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord) Source #
coerceLeqL :: forall n m l. (n :~: m) -> SNat l -> IsTrue (n <=? l) -> IsTrue (m <=? l) Source #
Since 1.0.0.0 (type changed)
coerceLeqR :: forall n m l. SNat l -> (n :~: m) -> IsTrue (l <=? n) -> IsTrue (l <=? m) Source #
Since 1.0.0.0 (type changed)
flipCmpNat :: SNat a -> SNat b -> FlipOrdering (CmpNat a b) :~: CmpNat b a Source #
leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> ((a :~: b) -> Void) -> CmpNat a b :~: 'LT Source #
congFlipOrdering :: (a :~: b) -> FlipOrdering a :~: FlipOrdering b Source #
cmpSuccStepR :: forall n m. SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT Source #
leqViewRefl :: SNat n -> LeqView n n Source #
leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> ((n :~: m) -> Void) -> IsTrue (Succ n <=? m) Source #
leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l) Source #
plusMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <=? m) -> IsTrue (l <=? k) -> IsTrue ((n + l) <=? (m + k)) Source #
plusMonotoneL :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue ((n + l) <=? (m + l)) Source #
plusMonotoneR :: SNat n -> SNat m -> SNat l -> IsTrue (m <=? l) -> IsTrue ((n + m) <=? (n + l)) Source #
plusCancelLeqR :: SNat n -> SNat m -> SNat l -> IsTrue ((n + l) <=? (m + l)) -> IsTrue (n <=? m) Source #
plusCancelLeqL :: SNat n -> SNat m -> SNat l -> IsTrue ((n + m) <=? (n + l)) -> IsTrue (m <=? l) Source #
minLargest :: SNat l -> SNat n -> SNat m -> IsTrue (l <=? n) -> IsTrue (l <=? m) -> IsTrue (l <=? Min n m) Source #
maxLeast :: SNat l -> SNat n -> SNat m -> IsTrue (n <=? l) -> IsTrue (m <=? l) -> IsTrue (Max n m <=? l) Source #
plusStrictMonotone :: SNat n -> SNat m -> SNat l -> SNat k -> IsTrue (n <? m) -> IsTrue (l <? k) -> IsTrue ((n + l) <? (m + k)) Source #
type (-.) n m = Subt n m (m <=? n) infixl 6 Source #
Natural subtraction, truncated to zero if m > n.
Various witnesses for orderings
type LeqWitness n m = IsTrue (n <=? m) Source #
Comparison via GADTs.
conversions between lax orders
propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m Source #