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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Generalize

Synopsis

- generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type)
- generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a)
- generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a

# Documentation

generalizeType :: Set QName -> TCM Type -> TCM ([Maybe QName], Type) Source #

Generalize a type over a set of (used) generalizable variables.

generalizeType' :: Set QName -> TCM (Type, a) -> TCM ([Maybe QName], Type, a) Source #

Allow returning additional information from the type checking action.

generalizeTelescope :: Map QName Name -> (forall a. (Telescope -> TCM a) -> TCM a) -> ([Maybe Name] -> Telescope -> TCM a) -> TCM a Source #

Generalize a telescope over a set of generalizable variables.