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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.Epic.Static

Description

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

Documentation

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) #