| Copyright | (c) 2016-2024 Rudy Matela |
|---|---|
| License | 3-Clause BSD (see the file LICENSE) |
| Maintainer | Rudy Matela <rudy@matela.com.br> |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Test.Speculate.SemiReason
Description
This module is part o Speculate.
Inequational (or semi-equational) reasoning.
Synopsis
- type Equation = (Expr, Expr)
- data Shy = Shy {
- sequations :: [Equation]
- sthy :: Thy
- emptyShy :: Shy
- updateSemiEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
- mapSemiEquations :: (Equation -> Equation) -> Shy -> Shy
- scompareE :: Shy -> Expr -> Expr -> Ordering
- lesser :: Shy -> Expr -> [Expr]
- greater :: Shy -> Expr -> [Expr]
- simplerThan :: Equation -> Shy -> Shy
- transConsequence :: Shy -> Equation -> Bool
- updateSEquationsBy :: ([Equation] -> [Equation]) -> Shy -> Shy
- stheorize :: Thy -> [Equation] -> Shy
- sides :: Shy -> [Expr]
- finalSemiEquations :: (Equation -> Bool) -> Instances -> (Expr -> Expr -> Bool) -> Shy -> [Equation]
- canonicalizeShyWith :: Instances -> Shy -> Shy
- canonicalizeSemiEquationWith :: Instances -> Equation -> Equation
Documentation
simplerThan :: Equation -> Shy -> Shy Source #
given a semi-equation (inequality), simplerThan restricts the Shy (SemiTheory) into only equations simpler than the given semi-equation or that are instances of simpler equations.
half-baked example:
x + 1 is simpler than x + y and it is returned.
(1 + 1) + 1 is more complex than x + y
but it is returned as well as it is an instance of x + 1.