Core.Case.Util

Definitions

record DataCon : Type

Totality: total
Visibility: public export
Constructor: 

MkDataCon : Name -> Int -> Nat -> DataCon

Projections:

.arity : DataCon -> Nat

.name : DataCon -> Name

.tag : DataCon -> Int

.name : DataCon -> Name

Visibility: public export

name : DataCon -> Name

Visibility: public export

.tag : DataCon -> Int

Visibility: public export

tag : DataCon -> Int

Visibility: public export

.arity : DataCon -> Nat

Visibility: public export

arity : DataCon -> Nat

Visibility: public export

getCons : Defs -> NF vars -> Core (List DataCon)

  Given a normalised type, get all the possible constructors for that
  type family, with their type, name, tag, and arity.

Visibility: export

mkAlt : FC -> CaseTree vars -> DataCon -> CaseAlt vars

Visibility: export

tagIs : Int -> CaseAlt vars -> Bool

Visibility: export