Agda-2.3.0: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.CompiledClause
type :-> key value = Map key valueSource
data Case c Source
Constructors
Fields
Instances
data CompiledClauses Source
Case n bs stands for a match on the n-th argument (counting from zero) with bs as the case branches.
Case n bs
n
bs
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.
Done xs b
b
xs
Absurd case.