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

Minimal complete definition

evaluate

Methods

evaluate :: a -> Compile TCM a

Instances

Evaluate Term

Methods

evaluate :: Term -> Compile TCM Term

Evaluate a => Evaluate [a]

Methods

evaluate :: [a] -> Compile TCM [a]

Evaluate a => Evaluate (Arg a)

Methods

evaluate :: Arg a -> Compile TCM (Arg a)

Evaluate a => Evaluate (Abs a)

Methods

evaluate :: Abs a -> Compile TCM (Abs a)

Evaluate a => Evaluate (Elim' a)

Methods

evaluate :: Elim' a -> Compile TCM (Elim' a)