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

Safe HaskellSafe-Infered

Agda.TypeChecking.CompiledClause

Documentation

type :-> key value = Map key value

data Case c

Constructors

Branches 

Instances

data CompiledClauses

Constructors

Case Int (Case CompiledClauses)

Case n bs stands for a match on the n-th argument (counting from zero) with bs as the case branches.

Done [Arg String] Term

Done xs b stands for the body b where the xs contains hiding and name suggestions for the free variables. This is needed to build lambdas on the right hand side for partial applications which can still reduce.

Fail

Absurd case.

litCase :: Literal -> c -> Case c

conCase :: QName -> c -> Case c

catchAll :: c -> Case c