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

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 :: Range -> 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 :: Nat -> Term -> a -> a
- swap01 :: TermSubst a => a -> a
- class EqualSy a where
  - equalSy :: a -> a -> Bool

# Documentation

abstractType Source #

Arguments

:: Range | Range of the `rewrite` expression, if any, otherwise empty.
-> Type | Type of the term to abstract.
-> Term | Term to abstract.
-> Type | Type to abstract in.
-> TCM Type | Type with hole (de Bruijn index 0) for the abstracted term.

`abstractType r 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 Args Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods isPrefixOf :: Args -> Args -> Maybe Elims Source #
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 #

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

class AbsTerm a where Source #

Methods

absTerm Source #

Arguments

:: Nat | De Bruijn index that should be the placeholder for the abstracted term.
-> Term | Term to abstract.
-> a | Where to abstract.
-> a | If the given de Bruijn index is free in the result, abstraction actually happened.

    subst j u . absTerm j u == id

#### Instances

Instances details

AbsTerm Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Level -> Level Source #
AbsTerm PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> PlusLevel -> PlusLevel Source #
AbsTerm Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Sort -> Sort Source #
AbsTerm Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Term -> Term Source #
AbsTerm Type Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Type -> Type Source #
AbsTerm a => AbsTerm (Arg a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Arg a -> Arg a Source #
(TermSubst a, AbsTerm a) => AbsTerm (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Abs a -> Abs a Source #
AbsTerm a => AbsTerm (Dom a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Dom a -> Dom a Source #
AbsTerm a => AbsTerm (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Elim' a -> Elim' a Source #
AbsTerm a => AbsTerm (Maybe a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> Maybe a -> Maybe a Source #
AbsTerm a => AbsTerm [a] Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> Term -> [a] -> [a] Source #
(AbsTerm a, AbsTerm b) => AbsTerm (a, b) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods absTerm :: Nat -> 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 Level Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Level -> Level -> Bool Source #
EqualSy PlusLevel Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: PlusLevel -> PlusLevel -> Bool Source #
EqualSy Sort Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Sort -> Sort -> Bool Source #
EqualSy Term Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Term -> Term -> Bool Source #
EqualSy Type Source # | Ignores sorts.
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Type -> Type -> 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 #
(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 #
EqualSy a => EqualSy (Elim' a) Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: Elim' a -> Elim' a -> Bool Source #
EqualSy a => EqualSy [a] Source # |
Instance details Defined in Agda.TypeChecking.Abstract Methods equalSy :: [a] -> [a] -> Bool Source #