Idris2Doc : Test.DepTyCheck.Gen.Emptiness

Test.DepTyCheck.Gen.Emptiness

(source)
Reexports
import public Language.Implicits.IfUnsolved
Definitions
data Emptiness : Type
  Totality: total
  Visibility: public export
  Constructors:
  
NonEmpty : Emptiness
  
MaybeEmpty : Emptiness

  Hints:
  
Alternative (GenAlternatives False em)
  
Antisymmetric Emptiness NoWeaker
  
Applicative (Gen em)
  
Applicative (GenAlternatives ne em)
  
Cast (LazyLst ne a) (GenAlternatives ne em a)
  
Connex Emptiness NoWeaker
  
Eq Emptiness
  
Functor (Gen em)
  
Functor (GenAlternatives ne em)
  
LinearOrder Emptiness NoWeaker
  
Monad (Gen em)
  
Monad (GenAlternatives True em)
  
Not (a `NoWeaker` b) -> b `NoWeaker` a
  
NonEmpty `NoWeaker` em
  
em `NoWeaker` em
  
Ord Emptiness
  
PartialOrder Emptiness NoWeaker
  
Preorder Emptiness NoWeaker
  
Reflexive Emptiness NoWeaker
  
StronglyConnex Emptiness NoWeaker
  
Transitive Emptiness NoWeaker
data NoWeaker : Emptiness -> Emptiness -> Type
  Totality: total
  Visibility: public export
  Constructors:
  
NN : NonEmpty `NoWeaker` NonEmpty
  
AS : em `NoWeaker` MaybeEmpty

  Hints:
  
Antisymmetric Emptiness NoWeaker
  
Connex Emptiness NoWeaker
  
LinearOrder Emptiness NoWeaker
  
Not (a `NoWeaker` b) -> b `NoWeaker` a
  
NonEmpty `NoWeaker` em
  
em `NoWeaker` em
  
PartialOrder Emptiness NoWeaker
  
Preorder Emptiness NoWeaker
  
Reflexive Emptiness NoWeaker
  
StronglyConnex Emptiness NoWeaker
  
Transitive Emptiness NoWeaker
  
Uninhabited (MaybeEmpty `NoWeaker` NonEmpty)

  Fixity Declaration: infix operator, level 6
transitive' : x `NoWeaker` y -> y `NoWeaker` z -> x `NoWeaker` z
  Totality: total
  Visibility: export
rev : Not (a `NoWeaker` b) -> b `NoWeaker` a
  Totality: total
  Visibility: export
nonEmptyIsStrongest : NonEmpty `NoWeaker` em
  Totality: total
  Visibility: export
maybeEmptyIsMinimal : (0 _ : MaybeEmpty `NoWeaker` em) -> em = MaybeEmpty
  Totality: total
  Visibility: export
nonEmptyIsMaximal : (0 _ : em `NoWeaker` NonEmpty) -> em = NonEmpty
  Totality: total
  Visibility: export
minMaybeEmptyLeft : (0 em : Emptiness) -> min MaybeEmpty em = MaybeEmpty
  Totality: total
  Visibility: export
minMaybeEmptyRight : (0 em : Emptiness) -> min em MaybeEmpty = MaybeEmpty
  Totality: total
  Visibility: export
minNonEmptyLeft : (0 em : Emptiness) -> min NonEmpty em = em
  Totality: total
  Visibility: export
minNonEmptyRight : (0 em : Emptiness) -> min em NonEmpty = em
  Totality: total
  Visibility: export
minSame : (0 em : Emptiness) -> min em em = em
  Totality: total
  Visibility: export
minNoWeaker : a1 `NoWeaker` a2 -> b1 `NoWeaker` b2 -> min a1 b1 `NoWeaker` min a2 b2
  Totality: total
  Visibility: export
minNoWeakerLeft : a `NoWeaker` b -> min a c `NoWeaker` min b c
  Totality: total
  Visibility: export
minNoWeakerRight : a `NoWeaker` b -> min c a `NoWeaker` min c b
  Totality: total
  Visibility: export
leftNoWeakerMin : a `NoWeaker` min a b
  Totality: total
  Visibility: export
rightNoWeakerMin : b `NoWeaker` min a b
  Totality: total
  Visibility: export
noWeakerReflexive : em `NoWeaker` em
  Totality: total
  Visibility: export