Decidable.Finite.Fin

Definitions

finiteDecEx : {0 p : Fin n -> Type} -> ((k : Fin n) -> Dec (p k)) -> Dec (k : Fin n ** p k)

  Given a decidable predicate on Fin n,
  it's decidable whether any number in Fin n satisfies it.

Visibility: public export

finiteDecAll : {0 p : Fin n -> Type} -> ((k : Fin n) -> Dec (p k)) -> Dec ((k : Fin n) -> p k)

  Given a decidable predicate on Fin n,
  it's decidable whether all numbers in Fin n satisfy it.

Visibility: public export