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

Safe Haskell	None
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.