Agda-2.4.0: A dependently typed functional programming language and proof assistant
Agda.Compiler.Epic.Static
Description
Find the places where the builtin static is used and do some normalisation there.
normaliseStatic :: CompiledClauses -> Compile TCM CompiledClausesSource
evaluateCC :: CompiledClauses -> Compile TCM CompiledClausesSource
etaExpand :: Term -> Compile TCM TermSource
class Evaluate a whereSource
Methods
evaluate :: a -> Compile TCM aSource
Instances