Syntax.PreorderReasoning.Generic

Definitions

data Step : (a -> a -> Type) -> a -> a -> Type

Totality: total
Visibility: public export
Constructor:

(...) : (y : a) -> leq x y -> Step leq x y

data FastDerivation : (a -> a -> Type) -> a -> a -> Type

Totality: total
Visibility: public export
Constructors:

(|~) : (x : a) -> FastDerivation leq x x
(<~) : FastDerivation leq x y -> Step leq y z -> FastDerivation leq x z

data DerivationType : FastDerivation leq x y -> Type

Totality: total
Visibility: public export
Constructors:

TrivialDerivation : DerivationType ((|~) x)
SingleStepDerivation : DerivationType ((|~) x <~ step)
NonTrivialDerivation : DerivationType ((der <~ step1) <~ step2)

derivationType : (der : FastDerivation leq x y) -> DerivationType der

Visibility: public export

0 Prerequisite : DerivationType der -> Type

Visibility: public export

inductivePrerequisite : (der : FastDerivation leq x y) -> (0 step1 : Step leq y z) -> (0 step2 : Step leq z w) -> Prerequisite (derivationType ((der <~ step1) <~ step2)) -> Prerequisite (derivationType (der <~ step1))

Visibility: public export

preorderPrerequisite : Preorder dom leq => (der : FastDerivation leq x y) -> Prerequisite (derivationType der)

Visibility: public export

CalcSmart : (der : FastDerivation leq x y) -> Prerequisite (derivationType der) => leq x y

  The Prerequisite for the derivation:
  0-length derivation: Reflexive dom leq
  1-length derivation: Unit (no prerequisite)
  2 steps of longer: Transitivity

Visibility: public export

CalcWith : Preorder dom leq => FastDerivation leq x y -> leq x y

Visibility: public export

(~~) : FastDerivation leq x y -> (0 _ : Step Equal y z) -> FastDerivation leq x z

Visibility: public export
Fixity Declarations:
infixl operator, level 0
infixl operator, level 0

(..<) : Symmetric a leq => (y : a) -> leq y x -> Step leq x y