ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Reduce.Monad

Synopsis

valueconstructorForm :: HasBuiltins m => Term -> m Term

valueenterClosure :: LensClosure c a => c -> (a -> ReduceM b) -> ReduceM b

methodgetConstInfo :: QName -> m Definition

Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.

valueaskR :: ReduceM ReduceEnv

valueapplyWhenVerboseS

Apply a function if a certain verbosity level is activated.

Precondition: The level must be non-negative.

Orphan instances

5 instances