Hoogle Search

Within LTS Haskell 24.52 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. addIsLeqLeft1 :: forall (n :: Natural) (n' :: Natural) (m :: Nat) . LeqProof (n + n') m -> LeqProof n m

   parameterized-utils	Data.Parameterized.NatRepr

   No documentation available.

2. addPrefixIsLeq :: forall f (m :: Natural) g (n :: Nat) . f m -> g n -> LeqProof n (m + n)

   parameterized-utils	Data.Parameterized.NatRepr

   No documentation available.

3. decideLeq :: forall (a :: Nat) (b :: Nat) . NatRepr a -> NatRepr b -> Either (LeqProof a b) (LeqProof a b -> Void)

   parameterized-utils	Data.Parameterized.NatRepr

   (<=) is a decidable relation on nats.

4. leqAdd :: forall f (m :: Nat) (n :: Nat) (p :: Natural) . LeqProof m n -> f p -> LeqProof m (n + p)

   parameterized-utils	Data.Parameterized.NatRepr

   Produce proof that adding a value to the larger element in an LeqProof is larger

5. leqAdd2 :: forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat) . LeqProof x_l x_h -> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)

   parameterized-utils	Data.Parameterized.NatRepr

   Add both sides of two inequalities

6. leqAddPos :: forall (m :: Natural) (n :: Natural) p q . (1 <= m, 1 <= n) => p m -> q n -> LeqProof 1 (m + n)

   parameterized-utils	Data.Parameterized.NatRepr

   No documentation available.

7. leqMulCongr :: forall (a :: Nat) (x :: Nat) (b :: Nat) (y :: Nat) . LeqProof a x -> LeqProof b y -> LeqProof (a * b) (x * y)

   parameterized-utils	Data.Parameterized.NatRepr

   Congruence rule for multiplication

8. leqMulPos :: forall p q (x :: Natural) (y :: Natural) . (1 <= x, 1 <= y) => p x -> q y -> LeqProof 1 (x * y)

   parameterized-utils	Data.Parameterized.NatRepr

   Multiplying two positive numbers results in a positive number.

9. leqRefl :: forall f (n :: Nat) . f n -> LeqProof n n

   parameterized-utils	Data.Parameterized.NatRepr

   Apply reflexivity to LeqProof

10. leqSub :: forall (m :: Nat) (n :: Nat) (p :: Nat) . LeqProof m n -> LeqProof p m -> LeqProof (m - p) n

    parameterized-utils	Data.Parameterized.NatRepr

    Produce proof that subtracting a value from the smaller element is smaller.

Page 379 of many | Previous | Next