Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.TypeChecking.CompiledClause
Synopsis
type :-> key value = Map key value
data Case c = Branches {
conBranches :: QName :-> c
litBranches :: Literal :-> c
catchAllBranch :: Maybe c
}
data CompiledClauses
= Case Int (Case CompiledClauses)
| Done Int Term
| Fail
compileClauses :: [Clauses] -> CompiledClauses
type Cl = ([Arg Pattern], ClauseBody)
type Cls = [Cl]
compile :: Cls -> CompiledClauses
nextSplit :: Cls -> Maybe Int
splitOn :: Int -> Cls -> Case Cls
splitC :: Int -> Cl -> Case Cl
Documentation
type :-> key value = Map key valueSource
data Case c Source
Constructors
Branches
conBranches :: QName :-> c
litBranches :: Literal :-> c
catchAllBranch :: Maybe c
data CompiledClauses Source
Constructors
Case Int (Case CompiledClauses)
Done Int Term
Fail
compileClauses :: [Clauses] -> CompiledClausesSource
Note that it is the translated clauses which are compiled, not the original ones.
type Cl = ([Arg Pattern], ClauseBody)Source
type Cls = [Cl]Source
compile :: Cls -> CompiledClausesSource
nextSplit :: Cls -> Maybe IntSource
splitOn :: Int -> Cls -> Case ClsSource
splitC :: Int -> Cl -> Case ClSource
Produced by Haddock version 2.6.1