Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Abstract

Contents

Equality of terms for the sake of with-abstraction.

Description

Functions for abstracting terms over other terms.

Synopsis

abstractType :: Type -> Term -> Type -> TCM Type
piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type
piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type
class IsPrefixOf a where
- isPrefixOf :: a -> a -> Maybe Elims
abstractTerm :: Type -> Term -> Type -> Term -> TCM Term
class AbsTerm a where
- absTerm :: Term -> a -> a
swap01 :: TermSubst a => a -> a
class EqualSy a where
- equalSy :: a -> a -> Bool

Documentation

abstractType :: Type -> Term -> Type -> TCM Type Source #

abstractType a v b[v] = b where a : v.

piAbstractTerm :: ArgInfo -> Term -> Type -> Type -> TCM Type Source #

piAbstractTerm NotHidden v a b[v] = (w : a) -> b[w] piAbstractTerm Hidden v a b[v] = {w : a} -> b[w]

piAbstract :: Arg (Term, EqualityView) -> Type -> TCM Type Source #

piAbstract (v, a) b[v] = (w : a) -> b[w]

For the inspect idiom, it does something special: @piAbstract (v, a) b[v] = (w : a) {w' : Eq a w v} -> b[w]

For rewrite, it does something special: piAbstract (prf, Eq a v v') b[v,prf] = (w : a) (w' : Eq a w v') -> b[w,w']

class IsPrefixOf a where Source #

isPrefixOf u v = Just es if v == u applyE es.

Methods

isPrefixOf :: a -> a -> Maybe Elims Source #

Instances

Instances details

IsPrefixOf Elims Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Elims -> Elims -> Maybe Elims Source #
IsPrefixOf Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Term -> Term -> Maybe Elims Source #
IsPrefixOf Args Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #

abstractTerm :: Type -> Term -> Type -> Term -> TCM Term Source #

class AbsTerm a where Source #

Methods

absTerm :: Term -> a -> a Source #

subst u . absTerm u == id

Instances

Instances details

AbsTerm PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> PlusLevel -> PlusLevel Source #
AbsTerm Level Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Level -> Level Source #
AbsTerm Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Sort -> Sort Source #
AbsTerm Type Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Type -> Type Source #
AbsTerm Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Term -> Term Source #
AbsTerm a => AbsTerm [a] Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> [a] -> [a] Source #
AbsTerm a => AbsTerm (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Maybe a -> Maybe a Source #
AbsTerm a => AbsTerm (Arg a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Arg a -> Arg a Source #
AbsTerm a => AbsTerm (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Elim' a -> Elim' a Source #
(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Abs a -> Abs a Source #
AbsTerm a => AbsTerm (Dom a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> Dom a -> Dom a Source #
(AbsTerm a, AbsTerm b) => AbsTerm (a, b) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Term -> (a, b) -> (a, b) Source #

swap01 :: TermSubst a => a -> a Source #

This swaps var 0 and var 1.

Equality of terms for the sake of with-abstraction.

class EqualSy a where Source #

Methods

equalSy :: a -> a -> Bool Source #

Instances

Instances details

EqualSy ArgInfo Source #	Ignore origin and free variables.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: ArgInfo -> ArgInfo -> Bool Source #
EqualSy PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: PlusLevel -> PlusLevel -> Bool Source #
EqualSy Level Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Level -> Level -> Bool Source #
EqualSy Sort Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
EqualSy Type Source #	Ignores sorts.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Type -> Type -> Bool Source #
EqualSy Term Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Term -> Term -> Bool Source #
EqualSy a => EqualSy [a] Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: [a] -> [a] -> Bool Source #
EqualSy a => EqualSy (Arg a) Source #	Ignores irrelevant arguments and modality. (And, of course, origin and free variables).
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Arg a -> Arg a -> Bool Source #
EqualSy a => EqualSy (Elim' a) Source #
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Elim' a -> Elim' a -> Bool Source #
(Subst a, EqualSy a) => EqualSy (Abs a) Source #	Ignores `absName`.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Abs a -> Abs a -> Bool Source #
EqualSy a => EqualSy (Dom a) Source #	Ignore the tactic.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Dom a -> Dom a -> Bool Source #