Idris2Doc : Decidable.HDecEq

Decidable.HDecEq

(source)
Reexports
import public Data.List.Quantifiers
import public Data.Maybe0
Definitions
interface HDecEq : Type -> Type
  Hemi-decidable equality.

  Parameters: a
Constructor: 
MkHDecEq

Methods:
  
hdecEq : (x : a) -> (y : a) -> Maybe0 (x = y)

Implementations:
  
HDecEq Bits8
  
HDecEq Bits16
  
HDecEq Bits32
  
HDecEq Bits64
  
HDecEq Int8
  
HDecEq Int16
  
HDecEq Int32
  
HDecEq Int64
  
HDecEq Integer
  
HDecEq Int
  
HDecEq Char
  
HDecEq String
  
HDecEq a => HDecEq (Maybe a)
  
HDecEq a => HDecEq b => HDecEq (Either a b)
  
HDecEq a => HDecEq b => HDecEq (a, b)
  
HDecEq Nat
  
HDecEq a => HDecEq (List a)
  
HDecEq a => HDecEq (SnocList a)
  
All (HDecEq . f) ks => HDecEq (All f ks)
  
All (HDecEq . f) ks => HDecEq (Any f ks)
hdecEq : HDecEq a => (x : a) -> (y : a) -> Maybe0 (x = y)
  Totality: total
  Visibility: public export