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

Safe HaskellSafe-Infered

Agda.Compiler.Epic.Static

Description

Find the places where the builtin static is used and do some normalisation there.

Documentation

normaliseStatic :: CompiledClauses -> Compile TCM CompiledClausesSource

evaluateCC :: CompiledClauses -> Compile TCM CompiledClausesSource

etaExpand :: Term -> Compile TCM TermSource

evaluateTerm :: Term -> Compile TCM TermSource