Agda.Compiler.Epic.Static

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

Documentation

normaliseStatic :: CompiledClauses -> Compile TCM CompiledClauses

evaluateCC :: CompiledClauses -> Compile TCM CompiledClauses

etaExpand :: Term -> Compile TCM Term

class Evaluate a where

Methods

evaluate :: a -> Compile TCM a

Instances

Evaluate Term

Evaluate a => Evaluate [a]

Evaluate a => Evaluate (Abs a)

Evaluate a => Evaluate (Elim' a)

Evaluate a => Evaluate (Arg a)