Decidable.HDec

Reexports

Definitions

interface HDec0 : (a : Type) -> (a -> Type) -> Type

  Hemi-decidability for erased predicates

Parameters: a, p
Methods:

hdec0 : (v : a) -> Maybe0 ((v `p`))

Implementations:

HDec0 (List Char) LeftTrimmed

HDec0 (List Char) RightTrimmed

HDec0 Integer (\{arg:0} => {arg:0} < x)

HDec0 Integer (\{arg:0} => x < {arg:0})

HDec0 Integer (\{arg:0} => {arg:0} <= x)

HDec0 Integer (\{arg:0} => x <= {arg:0})

HDec0 Int8 (\{arg:0} => {arg:0} < x)

HDec0 Int8 (\{arg:0} => x < {arg:0})

HDec0 Int8 (\{arg:0} => {arg:0} <= x)

HDec0 Int8 (\{arg:0} => x <= {arg:0})

HDec0 Int64 (\{arg:0} => {arg:0} < x)

HDec0 Int64 (\{arg:0} => x < {arg:0})

HDec0 Int64 (\{arg:0} => {arg:0} <= x)

HDec0 Int64 (\{arg:0} => x <= {arg:0})

HDec0 Int32 (\{arg:0} => {arg:0} < x)

HDec0 Int32 (\{arg:0} => x < {arg:0})

HDec0 Int32 (\{arg:0} => {arg:0} <= x)

HDec0 Int32 (\{arg:0} => x <= {arg:0})

HDec0 Int16 (\{arg:0} => {arg:0} < x)

HDec0 Int16 (\{arg:0} => x < {arg:0})

HDec0 Int16 (\{arg:0} => {arg:0} <= x)

HDec0 Int16 (\{arg:0} => x <= {arg:0})

HDec0 Char (\{arg:0} => {arg:0} < x)

HDec0 Char (\{arg:0} => x < {arg:0})

HDec0 Char (\{arg:0} => {arg:0} <= x)

HDec0 Char (\{arg:0} => x <= {arg:0})

HDec0 Bits8 (\{arg:0} => {arg:0} < x)

HDec0 Bits8 (\{arg:0} => x < {arg:0})

HDec0 Bits8 (\{arg:0} => {arg:0} <= x)

HDec0 Bits8 (\{arg:0} => x <= {arg:0})

HDec0 Bits64 (\{arg:0} => {arg:0} < x)

HDec0 Bits64 (\{arg:0} => x < {arg:0})

HDec0 Bits64 (\{arg:0} => {arg:0} <= x)

HDec0 Bits64 (\{arg:0} => x <= {arg:0})

HDec0 Bits32 (\{arg:0} => {arg:0} < x)

HDec0 Bits32 (\{arg:0} => x < {arg:0})

HDec0 Bits32 (\{arg:0} => {arg:0} <= x)

HDec0 Bits32 (\{arg:0} => x <= {arg:0})

HDec0 Bits16 (\{arg:0} => {arg:0} < x)

HDec0 Bits16 (\{arg:0} => x < {arg:0})

HDec0 Bits16 (\{arg:0} => {arg:0} <= x)

HDec0 Bits16 (\{arg:0} => x <= {arg:0})

HDec0 (List a) NonEmpty

HDec0 Nat (LTE n)

HDec0 Nat (\{arg:0} => LTE {arg:0} n)

HDec0 Nat IsSucc

HDecEq a => HDec0 a (\{arg:0} => v = {arg:0})

HDec0 Bits16 (\{arg:0} => x <= {arg:0})

HDec0 Bits16 (\{arg:0} => {arg:0} <= x)

HDec0 Bits16 (\{arg:0} => x < {arg:0})

HDec0 Bits16 (\{arg:0} => {arg:0} < x)

HDec0 a p => HDec0 (List a) (All p)

HDec0 a p => HDec0 (List a) (Any p)

HDec0 a Always

HDec0 a Never

HDec0 a p => HDec0 a q => HDec0 a (p && q)

HDec0 a p => HDec0 a q => HDec0 a (p || q)

HDec0 a p => HDec0 b (On p f)

HDec0 a (Holds f)

HDec0 e p => HDec0 t (Const p v)

hdec0 : HDec0 a p => (v : a) -> Maybe0 ((v `p`))

Totality: total
Visibility: public export

hdec0All : HDec0 a p => (vs : List a) -> Maybe0 (All p vs)

Totality: total
Visibility: public export

hdec0Any : HDec0 a p => (vs : List a) -> Maybe0 (Any p vs)

Totality: total
Visibility: public export

interface HDec : (a : Type) -> (a -> Type) -> Type

  Hemi-decidability for non-erased predicates

Parameters: a, p
Methods:

hdec : (v : a) -> Maybe ((v `p`))

Implementations:

HDec (List Char) LeftTrimmed

HDec (List Char) RightTrimmed

HDec (List a) NonEmpty

HDec Nat (LTE n)

HDec Nat (\{arg:0} => LTE {arg:0} n)

HDecEq a => HDec a (\{arg:0} => v = {arg:0})

HDec a p => HDec (List a) (All p)

HDec a Always

HDec a Never

HDec a p => HDec a q => HDec a (p && q)

HDec a p => HDec a q => HDec a (p || q)

HDec a p => HDec b (On p f)

HDec a (Holds f)

hdec : HDec a p => (v : a) -> Maybe ((v `p`))

Totality: total
Visibility: public export

hdecAll : HDec a p => (vs : List a) -> Maybe (All p vs)

Totality: total
Visibility: public export