Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Auto.Syntax

Synopsis

Documentation

type UId o = Metavar (Exp o) (RefInfo o) Source #

Unique identifiers for variable occurrences in unification.

data HintMode Source #

Constructors

HMNormal 
HMRecCall 

data RefInfo o Source #

The concrete instance of the blk parameter in Metavar. I.e., the information passed to the search control.

Constructors

RIEnv 

Fields

RIMainInfo 

Fields

  • riMainCxtLength :: Nat

    Size of typing context in which meta was created.

  • riMainType :: HNExp o

    Head normal form of type of meta.

  • riMainIota :: Bool

    True if iota steps performed when normalising target type (used to put cost when traversing a definition by construction instantiation).

RIUnifInfo [CAction o] (HNExp o) 
RICopyInfo (ICExp o) 
RIIotaStep Bool 
RIInferredTypeUnknown 
RINotConstructor 
RIUsedVars [UId o] [Elr o] 
RIPickSubsvar 
RIEqRState EqReasoningState 
RICheckElim Bool 
RICheckProjIndex [ConstRef o] 

Instances

Instances details
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b Source #

LocalTerminationEnv (MArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

LocalTerminationEnv (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #

Replace (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o) Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #

Refinable (ArgList o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #

Refinable (ConstRef o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

Refinable (Exp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #

Refinable (ICExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #

(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (MM t (RefInfo o)) Source #

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe () Source #

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

Replace t u => Replace (MM t (RefInfo o)) u Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (MM t (RefInfo o)) u Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u Source #

type ReplaceWith (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o
type UnifiesTo (MM t (RefInfo o)) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type UnifiesTo (MM t (RefInfo o)) = o
type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o
type ReplaceWith (MM t (RefInfo o)) u Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

type MyPB o = PB (RefInfo o) Source #

type MyMB a o = MB a (RefInfo o) Source #

type Nat = Int Source #

data MId Source #

Constructors

Id String 
NoId 

Instances

Instances details
Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

data Abs a Source #

Abstraction with maybe a name.

Different from Agda, where there is also info whether function is constant.

Constructors

Abs MId a 

Instances

Instances details
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Abs0 a -> MOT (Abs b) Source #

Lift t => Lift (Abs t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Abs t -> Abs t Source #

Unify t => Unify (Abs t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Abs t) Source #

Methods

unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe () Source #

notequal' :: Abs t -> Abs t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool Source #

ExpandMetas t => ExpandMetas (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Abs t -> IO (Abs t) Source #

FreeVars t => FreeVars (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat Source #

MetaliseOKH t => MetaliseOKH (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Abs t -> IO (Abs t) Source #

Renaming t => Renaming (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #

Replace t u => Replace (Abs t) (Abs u) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Abs t) (Abs u) Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (Abs t) (Abs u)) -> Abs t -> Reader (Nat, Nat) (Abs u) Source #

type UnifiesTo (Abs t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type UnifiesTo (Abs t) = UnifiesTo t
type ReplaceWith (Abs t) (Abs u) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u

data ConstDef o Source #

Constant signatures.

Constructors

ConstDef 

Fields

Instances

Instances details
Refinable (ConstRef o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

data DeclCont o Source #

Constant definitions.

type Clause o = ([Pat o], MExp o) Source #

data Pat o Source #

Constructors

PatConApp (ConstRef o) [Pat o] 
PatVar String 
PatExp

Dot pattern.

Instances

Instances details
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM (Arg Pattern) (Pat O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

data Elr o Source #

Head of application (elimination).

Constructors

Var Nat 
Const (ConstRef o) 

Instances

Instances details
FreeVars (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat Source #

Renaming (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #

Weakening (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Elr o -> Elr o Source #

Eq (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

(==) :: Elr o -> Elr o -> Bool #

(/=) :: Elr o -> Elr o -> Bool #

data Sort Source #

Constructors

Set Nat 
UnknownSort 
Type 

data Exp o Source #

Agsy's internal syntax.

Constructors

App 

Fields

Lam Hiding (Abs (MExp o))

Lambda with hiding information.

Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))

True if possibly dependent (var not known to not occur). False if non-dependent.

Sort Sort 
AbsurdLambda Hiding

Absurd lambda with hiding information.

Instances

Instances details
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion MOT (Exp O) Term Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term Source #

Conversion MOT (Exp O) Type Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Lift (Exp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Exp o -> Exp o Source #

LocalTerminationEnv (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #

Unify (Exp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Exp o) Source #

Methods

unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe () Source #

notequal' :: Exp o -> Exp o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool Source #

Trav (Exp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (Exp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()) -> Exp o -> m () Source #

ExpandMetas (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Exp o -> IO (Exp o) Source #

FreeVars (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat Source #

MetaliseOKH (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Exp o -> IO (Exp o) Source #

Renaming (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #

Replace (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o) Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #

Refinable (Exp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #

Refinable (ICExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

type UnifiesTo (Exp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type UnifiesTo (Exp o) = o
type Block (Exp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (Exp o) = RefInfo o
type ReplaceWith (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o
type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

type MExp o = MM (Exp o) (RefInfo o) Source #

"Maybe expression": Expression or reference to meta variable.

data ArgList o Source #

Constructors

ALNil

No more eliminations.

ALCons Hiding (MExp o) (MArgList o)

Application and tail.

ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)

proj pre args, projfcn idx, tail

ALConPar (MArgList o)

Constructor parameter (missing in Agda). Agsy has monomorphic constructors. Inserted to cover glitch of polymorphic constructor applications coming from Agda

Instances

Instances details
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Lift (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> ArgList o -> ArgList o Source #

LocalTerminationEnv (MArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Unify (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (ArgList o) Source #

Methods

unify' :: ArgList o -> ArgList o -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe () Source #

notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool Source #

Trav (ArgList o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (ArgList o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()) -> ArgList o -> m () Source #

ExpandMetas (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: ArgList o -> IO (ArgList o) Source #

FreeVars (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

MetaliseOKH (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: ArgList o -> IO (ArgList o) Source #

Renaming (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #

Replace (ArgList o) (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (ArgList o) (ArgList o) Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (ArgList o) (ArgList o)) -> ArgList o -> Reader (Nat, Nat) (ArgList o) Source #

Refinable (ArgList o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #

type UnifiesTo (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type UnifiesTo (ArgList o) = o
type Block (ArgList o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (ArgList o) = RefInfo o
type ReplaceWith (ArgList o) (ArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (ArgList o) (ArgList o) = o

type MArgList o = MM (ArgList o) (RefInfo o) Source #

data WithSeenUIds a o Source #

Constructors

WithSeenUIds 

Fields

data HNExp' o Source #

Constructors

HNApp (Elr o) (ICArgList o) 
HNLam Hiding (Abs (ICExp o)) 
HNPi Hiding Bool (ICExp o) (Abs (ICExp o)) 
HNSort Sort 

data HNArgList o Source #

Head-normal form of ICArgList. First entry is exposed.

Q: Why are there no projection eliminations?

data ICArgList o Source #

Lazy concatenation of argument lists under explicit substitutions.

Constructors

CALNil 
CALConcat (Clos (MArgList o) o) (ICArgList o) 

Instances

Instances details
Weakening (ICArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> ICArgList o -> ICArgList o Source #

type ICExp o = Clos (MExp o) o Source #

An expression a in an explicit substitution [CAction a].

data Clos a o Source #

Constructors

Clos [CAction o] a 

Instances

Instances details
Refinable (ICExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

Weakening (Clos a o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Clos a o -> Clos a o Source #

type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

type CExp o = TrBr (ICExp o) o Source #

data TrBr a o Source #

Constructors

TrBr [MExp o] a 

Instances

Instances details
Trav (TrBr a o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (TrBr a o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()) -> TrBr a o -> m () Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

Weakening a => Weakening (TrBr a o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> TrBr a o -> TrBr a o Source #

type Block (TrBr a o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (TrBr a o) = RefInfo o
type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

data CAction o Source #

Entry of an explicit substitution.

An explicit substitution is a list of CActions. This is isomorphic to the usual presentation where Skip and Weak would be constructors of exp. substs.

Constructors

Sub (ICExp o)

Instantation of variable.

Skip

For going under a binder, often called Lift.

Weak Nat

Shifting substitution (going to a larger context).

type Ctx o = [(MId, CExp o)] Source #

type EE = IO Source #

class MetaliseOKH t where Source #

Methods

metaliseOKH :: t -> IO t Source #

Instances

Instances details
MetaliseOKH t => MetaliseOKH (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Abs t -> IO (Abs t) Source #

MetaliseOKH (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: ArgList o -> IO (ArgList o) Source #

MetaliseOKH (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Exp o -> IO (Exp o) Source #

MetaliseOKH t => MetaliseOKH (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: MM t a -> IO (MM t a) Source #

class ExpandMetas t where Source #

Methods

expandMetas :: t -> IO t Source #

Instances

Instances details
ExpandMetas t => ExpandMetas (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Abs t -> IO (Abs t) Source #

ExpandMetas (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: ArgList o -> IO (ArgList o) Source #

ExpandMetas (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Exp o -> IO (Exp o) Source #

ExpandMetas t => ExpandMetas (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: MM t a -> IO (MM t a) Source #

sub :: MExp o -> CExp o -> CExp o Source #

subi :: MExp o -> ICExp o -> ICExp o Source #

weak :: Weakening t => Nat -> t -> t Source #

class Weakening t where Source #

Methods

weak' :: Nat -> t -> t Source #

Instances

Instances details
Weakening (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Elr o -> Elr o Source #

Weakening (ICArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> ICArgList o -> ICArgList o Source #

Weakening (Clos a o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Clos a o -> Clos a o Source #

Weakening a => Weakening (TrBr a o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> TrBr a o -> TrBr a o Source #

doclos :: [CAction o] -> Nat -> Either Nat (ICExp o) Source #

Substituting for a variable.

freeVars :: FreeVars t => t -> Set Nat Source #

FreeVars class and instances

class FreeVars t where Source #

Methods

freeVarsOffset :: Nat -> t -> Set Nat Source #

Instances

Instances details
FreeVars t => FreeVars (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat Source #

FreeVars (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

FreeVars (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat Source #

FreeVars (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat Source #

FreeVars t => FreeVars (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat Source #

(FreeVars a, FreeVars b) => FreeVars (a, b) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> (a, b) -> Set Nat Source #

rename :: Renaming t => (Nat -> Nat) -> t -> t Source #

Renaming Typeclass and instances

class Renaming t where Source #

Methods

renameOffset :: Nat -> (Nat -> Nat) -> t -> t Source #

Instances

Instances details
Renaming (CSPatI o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o Source #

Renaming t => Renaming (HI t) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t Source #

Renaming t => Renaming (Abs t) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #

Renaming (ArgList o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #

Renaming (Elr o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #

Renaming (Exp o) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #

Renaming t => Renaming (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a Source #

(Renaming a, Renaming b) => Renaming (a, b) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> (a, b) -> (a, b) Source #