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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.Epic.Static

Description

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

Documentation

normaliseStatic :: CompiledClauses -> Compile TCM CompiledClauses Source

evaluateCC :: CompiledClauses -> Compile TCM CompiledClauses Source

etaExpand :: Term -> Compile TCM Term Source

class Evaluate a where Source

Methods

evaluate :: a -> Compile TCM a Source

Instances