Data.Enum

Reexports

Definitions

record Index : Bits32 -> Type

Totality: total
Visibility: public export
Constructor: 

I : (val : Bits32) -> {auto 0 _ : val < n} -> Index n

Projections:

0 .prf : ({rec:0} : Index n) -> val {rec:0} < n

.val : Index n -> Bits32

Hints:

Cast (Index n) Integer

Cast (Index n) Bits32

Eq (Index n)

Ord (Index n)

Show (Index n)

.val : Index n -> Bits32

Totality: total
Visibility: public export

val : Index n -> Bits32

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Index n) -> val {rec:0} < n

Totality: total
Visibility: public export

0 prf : ({rec:0} : Index n) -> val {rec:0} < n

Totality: total
Visibility: public export

tryIndex : Bits32 -> Maybe (Index r)

Totality: total
Visibility: export

fromInteger : (n : Integer) -> {auto 0 _ : cast n < r} -> Index r

Totality: total
Visibility: public export

Zero : {auto 0 _ : 0 < n} -> Index n

Totality: total
Visibility: public export

0 ltProof : (v : Bits32) -> {auto 0 _ : v < n} -> lt (cast v) (cast n) = True

Totality: total
Visibility: export

toFin : Index n -> Fin (cast n)

Totality: total
Visibility: export

interface Enum : Type -> Bits32 -> Type

  Verified enumerations.
  
  Provides a function for converting a value of the given type to an
  `Index n` of the given size.
  
  In addition, proves that `Finite.value` holds every value there is and
  that `toIndex` is injective.
  
  With these proofs we can use a value of type `t` as an index into a
  (potentially dependent) array.

Parameters: t, n
Constraints: Finite t
Constructor: 

MkEnum

Methods:

toIndex : t -> Index n

0 toIndexInjective : (x : t) -> (y : t) -> toIndex x = toIndex y -> x = y

0 valuesComplete : (x : t) -> Elem x values

Implementations:

Enum Bool 2

Enum Ordering 3

toIndex : Enum t n => t -> Index n

Totality: total
Visibility: public export

0 toIndexInjective : {auto __con : Enum t n} -> (x : t) -> (y : t) -> toIndex x = toIndex y -> x = y

Totality: total
Visibility: public export

0 valuesComplete : {auto __con : Enum t n} -> (x : t) -> Elem x values

Totality: total
Visibility: public export

enumToFin : Enum t n => t -> Fin (cast n)

Totality: total
Visibility: export

enumToBits32 : Enum t n => t -> Bits32

Totality: total
Visibility: export

enumToInteger : Enum t n => t -> Integer

Totality: total
Visibility: export

inList : HDecEq i => i -> List i -> Bool

Totality: total
Visibility: public export

0 inListImpliesElem : {auto {conArg:9856} : HDecEq i} -> (v : i) -> inList v is = True -> Elem v is

Totality: total
Visibility: export