Agda-2.2.6: A dependently typed functional programming language and proof assistant

Agda.Compiler.Alonzo.PatternMonad

Documentation

type Defs = Map QName DefinitionSource

data PState Source

Constructors

PSt 

Fields

cnt :: Int
 
vars :: [Int]
 
lst :: [HsPat]
 
clause :: Clause
 
defs :: Defs
 

initPState :: Clause -> Defs -> PStateSource

type PM a = StateT PState TCM aSource

getPDefs :: PM DefsSource

getPcnt :: PM IntSource

getPlst :: PM [HsPat]Source

getPclause :: PM ClauseSource

putPlst :: [HsPat] -> PM ()Source

putPcnt :: Int -> PM ()Source

incPcnt :: PM ()Source

addWildcard :: PM ()Source

addVar :: PM ()Source