| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Syntax.Internal
Contents
Synopsis
- type Args = [Arg Term]
- type Type = Type' Term
- data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: NAPs
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Bool
- clauseExact :: Maybe Bool
- clauseRecursive :: Maybe Bool
- clauseUnreachable :: Maybe Bool
- clauseEllipsis :: ExpandedEllipsis
- clauseWhereModule :: Maybe ModuleName
- data Term
- type Pattern = Pattern' PatVarName
- type Telescope = Tele (Dom Type)
- type Substitution = Substitution' Term
- data Dom' t e = Dom {}
- type Dom = Dom' Term
- type Level = Level' Term
- type Elim = Elim' Term
- type Sort = Sort' Term
- type DataOrRecord = DataOrRecord' PatternOrCopattern
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# (Substitution' a)
- | Strengthen Impossible !Int (Substitution' a)
- | Wk !Int (Substitution' a)
- | Lift !Int (Substitution' a)
- data Abs a
- class LensSort a where
- type Elims = [Elim]
- class TermSize a where
- type Blocked = Blocked' Term
- type NotBlocked = NotBlocked' Term
- type NamedArgs = [NamedArg Term]
- data DataOrRecord' p
- data ConHead = ConHead {
- conName :: QName
- conDataRecord :: DataOrRecord
- conInductive :: Induction
- conFields :: [Arg QName]
- class LensConName a where
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
- type ConInfo = ConOrigin
- data Type'' t a = El {}
- data Sort' t
- type Type' a = Type'' Term a
- data Tele a
- data UnivSize
- data Level' t = Max !Integer [PlusLevel' t]
- data PlusLevel' t = Plus !Integer t
- type PlusLevel = PlusLevel' Term
- type LevelAtom = Term
- newtype BraveTerm = BraveTerm {}
- type Blocked_ = Blocked ()
- type NAPs = [NamedArg DeBruijnPattern]
- type DeBruijnPattern = Pattern' DBPatVar
- type PatVarName = ArgName
- data PatternInfo = PatternInfo {
- patOrigin :: PatOrigin
- patAsNames :: [Name]
- data PatOrigin
- = PatOSystem
- | PatOSplit
- | PatOVar Name
- | PatODot
- | PatOWild
- | PatOCon
- | PatORec
- | PatOLit
- | PatOAbsurd
- data Pattern' x
- = VarP PatternInfo x
- | DotP PatternInfo Term
- | ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]
- | LitP PatternInfo Literal
- | ProjP ProjOrigin QName
- | IApplyP PatternInfo Term Term x
- | DefP PatternInfo QName [NamedArg (Pattern' x)]
- data ConPatternInfo = ConPatternInfo {
- conPInfo :: PatternInfo
- conPRecord :: Bool
- conPFallThrough :: Bool
- conPType :: Maybe (Arg Type)
- conPLazy :: Bool
- data DBPatVar = DBPatVar {}
- class PatternVars a where
- type PatternVarOut a
- patternVars :: a -> [Arg (Either (PatternVarOut a) Term)]
- type PatternSubstitution = Substitution' DeBruijnPattern
- data EqualityView
- data EqualityTypeData = EqualityTypeData {}
- data PathView
- data IntervalView
- type DummyTermKind = String
- type ListTel' a = [Dom (a, Type)]
- type ListTel = ListTel' ArgName
- class TelToArgs a where
- class SgTel a where
- class Suggest a where
- suggestName :: a -> Maybe String
- data Suggestion = forall a.Suggest a => Suggestion a
- type family TypeOf a
- pattern Prop :: Level' t -> Sort' t
- pattern Type :: Level' t -> Sort' t
- pattern SSet :: Level' t -> Sort' t
- pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView
- pattern ClosedLevel :: Integer -> Level
- var :: Nat -> Term
- litP :: Literal -> Pattern' a
- varP :: a -> Pattern' a
- mkType :: Integer -> Sort
- telToList :: Tele (Dom t) -> [Dom (ArgName, t)]
- arity :: Type -> Nat
- argFromDom :: Dom' t a -> Arg a
- namedArgFromDom :: Dom' t a -> NamedArg a
- domFromArg :: Arg a -> Dom a
- domFromNamedArg :: NamedArg a -> Dom a
- defaultDom :: a -> Dom a
- defaultArgDom :: ArgInfo -> a -> Dom a
- defaultNamedArgDom :: ArgInfo -> String -> a -> Dom a
- isStrictDataSort :: Sort' t -> Bool
- clausePats :: Clause -> [Arg DeBruijnPattern]
- patVarNameToString :: PatVarName -> String
- nameToPatVarName :: Name -> PatVarName
- defaultPatternInfo :: PatternInfo
- dotP :: Term -> Pattern' a
- namedVarP :: PatVarName -> Named_ Pattern
- namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern
- absurdP :: Int -> DeBruijnPattern
- absurdPatternName :: PatVarName
- noConPatternInfo :: ConPatternInfo
- toConPatternInfo :: ConInfo -> ConPatternInfo
- fromConPatternInfo :: ConPatternInfo -> ConInfo
- patternInfo :: Pattern' x -> Maybe PatternInfo
- patternOrigin :: Pattern' x -> Maybe PatOrigin
- properlyMatching :: Pattern' a -> Bool
- properlyMatching' :: Bool -> Bool -> Pattern' a -> Bool
- eqtSort :: EqualityView -> Sort
- eqtName :: EqualityView -> QName
- eqtParams :: EqualityView -> Args
- eqtType :: EqualityView -> Arg Term
- eqtLhs :: EqualityView -> Arg Term
- eqtRhs :: EqualityView -> Arg Term
- isEqualityType :: EqualityView -> Bool
- isPathType :: PathView -> Bool
- isIOne :: IntervalView -> Bool
- absurdBody :: Abs Term
- isAbsurdBody :: Abs Term -> Bool
- isAbsurdPatternName :: PatVarName -> Bool
- dontCare :: Term -> Term
- dummyLocName :: CallStack -> String
- dummyTermWith :: DummyTermKind -> CallStack -> Term
- dummyLevel :: CallStack -> Level
- atomicLevel :: t -> Level' t
- dummyTerm :: CallStack -> Term
- __DUMMY_TERM__ :: HasCallStack => Term
- __DUMMY_LEVEL__ :: HasCallStack => Level
- dummySort :: CallStack -> Sort
- __DUMMY_SORT__ :: HasCallStack => Sort
- dummyType :: CallStack -> Type
- __DUMMY_TYPE__ :: HasCallStack => Type
- dummyDom :: CallStack -> Dom Type
- __DUMMY_DOM__ :: HasCallStack => Dom Type
- varSort :: Int -> Sort
- tmSort :: Term -> Sort
- tmSSort :: Term -> Sort
- levelPlus :: Integer -> Level -> Level
- levelSuc :: Level -> Level
- mkProp :: Integer -> Sort
- mkSSet :: Integer -> Sort
- isSort :: Term -> Maybe Sort
- impossibleTerm :: CallStack -> Term
- mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a)
- mapAbsNames :: (ArgName -> ArgName) -> Tele a -> Tele a
- replaceEmptyName :: ArgName -> Tele a -> Tele a
- telFromList' :: (a -> ArgName) -> ListTel' a -> Telescope
- telFromList :: ListTel -> Telescope
- listTel :: Lens' Telescope ListTel
- stripDontCare :: Term -> Term
- suggests :: [Suggestion] -> String
- unSpine :: Term -> Term
- unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- pDom :: LensHiding a => a -> Doc -> Doc
- prettyPrecLevelSucs :: Int -> Integer -> (Int -> Doc) -> Doc
- module Agda.Syntax.Internal.Blockers
- module Agda.Syntax.Internal.Elim
- module Agda.Syntax.Internal.Univ
- module Agda.Syntax.Abstract.Name
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- newtype ProblemId = ProblemId Nat
Documentation
A clause is a list of patterns and the clause body.
The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.
clauseTel ~ permute clausePerm (patternVars namedClausePats)
Terms in dot patterns are valid in the clause telescope.
For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!
Constructors
| Clause | |
Fields
| |
Instances
Raw values.
Def is used for both defined and undefined constants.
Assume there is a type declaration and a definition for
every constant, even if the definition is an empty
list of clauses.
Constructors
| Var !Int Elims |
|
| Lam ArgInfo (Abs Term) | Terms are beta normal. Relevance is ignored |
| Lit Literal | |
| Def QName Elims |
|
| Con ConHead ConInfo Elims |
|
| Pi (Dom Type) (Abs Type) | dependent or non-dependent function space |
| Sort Sort | |
| Level Level | |
| MetaV !MetaId Elims | |
| DontCare Term | Irrelevant stuff in relevant position, but created
in an irrelevant context. Basically, an internal
version of the irrelevance axiom |
| Dummy String Elims | A (part of a) term or type which is only used for internal purposes.
Replaces the |
Instances
Arguments
| = Pattern' PatVarName | The |
type Substitution = Substitution' Term Source #
Similar to Arg, but we need to distinguish
an irrelevance annotation in a function domain
(the domain itself is not irrelevant!)
from an irrelevant argument.
Dom is used in Pi of internal syntax, in Context and Telescope.
Arg is used for actual arguments (Var, Con, Def etc.)
and in Abstract syntax and other situations.
- cubical
- When
annFinite (argInfoAnnotation domInfo) = Truefor the domain of aPitype, the elements should be compared by tabulating the domain type. Only supported in case the domain type is primIsOne, to obtain the correct equality for partial elements.
Constructors
| Dom | |
Instances
data Substitution' a Source #
Substitutions.
Constructors
| IdS | Identity substitution.
|
| EmptyS Impossible | Empty substitution, lifts from the empty context. First argument is |
| a :# (Substitution' a) infixr 4 | Substitution extension, ` |
| Strengthen Impossible !Int (Substitution' a) | Strengthening substitution. First argument is |
| Wk !Int (Substitution' a) | Weakening substitution, lifts to an extended context.
|
| Lift !Int (Substitution' a) | Lifting substitution. Use this to go under a binder.
|
Instances
Binder.
Abs: The bound variable might appear in the body.
NoAbs is pseudo-binder, it does not introduce a fresh variable,
similar to the const of Haskell.
Constructors
| Abs | The body has (at least) one free variable.
Danger: |
| NoAbs | |
Instances
class LensSort a where Source #
Minimal complete definition
class TermSize a where Source #
The size of a term is roughly the number of nodes in its syntax tree. This number need not be precise for logical correctness of Agda, it is only used for reporting (and maybe decisions regarding performance).
Not counting towards the term size are:
- sort and color annotations,
- projections.
Minimal complete definition
type NotBlocked = NotBlocked' Term Source #
data DataOrRecord' p Source #
Instances
Store the names of the record fields in the constructor. This allows reduction of projection redexes outside of TCM. For instance, during substitution and application.
Constructors
| ConHead | |
Fields
| |
Instances
class LensConName a where Source #
Minimal complete definition
Methods
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
Instances
| LensConName ConHead Source # | |
Defined in Agda.Syntax.Internal | |
Types are terms with a sort annotation.
Instances
Sorts.
Constructors
| Univ Univ (Level' t) |
|
| Inf Univ !Integer |
|
| SizeUniv |
|
| LockUniv |
|
| LevelUniv |
|
| IntervalUniv |
|
| PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) | Sort of the pi type. |
| FunSort (Sort' t) (Sort' t) | Sort of a (non-dependent) function type. |
| UnivSort (Sort' t) | Sort of another sort. |
| MetaS !MetaId [Elim' t] | |
| DefS QName [Elim' t] | A postulated sort. |
| DummyS String | A (part of a) term or type which is only used for internal purposes.
Replaces the abuse of |
Instances
Sequence of types. An argument of the first type is bound in later types and so on.
Instances
Instances
A level is a maximum expression of a closed level and 0..n
PlusLevel expressions each of which is an atom plus a number.
Constructors
| Max !Integer [PlusLevel' t] |
Instances
data PlusLevel' t Source #
Instances
type PlusLevel = PlusLevel' Term Source #
Newtypes for terms that produce a dummy, rather than crash, when applied to incompatible eliminations.
Instances
| Apply BraveTerm Source # | |
| Subst BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |
| DeBruijn BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute | |
| Show BraveTerm Source # | |
| type SubstArg BraveTerm Source # | |
Defined in Agda.TypeChecking.Substitute | |
type NAPs = [NamedArg DeBruijnPattern] Source #
Named pattern arguments.
type DeBruijnPattern = Pattern' DBPatVar Source #
type PatVarName = ArgName Source #
Pattern variables.
data PatternInfo Source #
Constructors
| PatternInfo | |
Fields
| |
Instances
| KillRange PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods | |
| EmbPrj PatternInfo Source # | |
| Generic PatternInfo Source # | |
Defined in Agda.Syntax.Internal Associated Types type Rep PatternInfo :: Type -> Type # | |
| Show PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> PatternInfo -> ShowS # show :: PatternInfo -> String # showList :: [PatternInfo] -> ShowS # | |
| NFData PatternInfo Source # | |
Defined in Agda.Syntax.Internal Methods rnf :: PatternInfo -> () # | |
| Eq PatternInfo Source # | |
Defined in Agda.Syntax.Internal | |
| type Rep PatternInfo Source # | |
Defined in Agda.Syntax.Internal type Rep PatternInfo = D1 ('MetaData "PatternInfo" "Agda.Syntax.Internal" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" 'False) (C1 ('MetaCons "PatternInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "patOrigin") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatOrigin) :*: S1 ('MetaSel ('Just "patAsNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Name]))) | |
Origin of the pattern: what did the user write in this position?
Constructors
| PatOSystem | Pattern inserted by the system |
| PatOSplit | Pattern generated by case split |
| PatOVar Name | User wrote a variable pattern |
| PatODot | User wrote a dot pattern |
| PatOWild | User wrote a wildcard pattern |
| PatOCon | User wrote a constructor pattern |
| PatORec | User wrote a record pattern |
| PatOLit | User wrote a literal pattern |
| PatOAbsurd | User wrote an absurd pattern |
Instances
Patterns are variables, constructors, or wildcards.
QName is used in ConP rather than Name since
a constructor might come from a particular namespace.
This also meshes well with the fact that values (i.e.
the arguments we are matching with) use QName.
Constructors
| VarP PatternInfo x | x |
| DotP PatternInfo Term | .t |
| ConP ConHead ConPatternInfo [NamedArg (Pattern' x)] |
|
| LitP PatternInfo Literal | E.g. |
| ProjP ProjOrigin QName | Projection copattern. Can only appear by itself. |
| IApplyP PatternInfo Term Term x | Path elimination pattern, like |
| DefP PatternInfo QName [NamedArg (Pattern' x)] | Used for HITs, the QName should be the one from primHComp. |
Instances
data ConPatternInfo Source #
The ConPatternInfo states whether the constructor belongs to
a record type (True) or data type (False).
In the former case, the PatOrigin of the conPInfo says
whether the record pattern orginates from the expansion of an
implicit pattern.
The Type is the type of the whole record pattern.
The scope used for the type is given by any outer scope
plus the clause's telescope (clauseTel).
Constructors
| ConPatternInfo | |
Fields
| |
Instances
Type used when numbering pattern variables.
Constructors
| DBPatVar | |
Fields
| |
Instances
class PatternVars a where Source #
Extract pattern variables in left-to-right order.
A DotP is also treated as variable (see docu for Clause).
Associated Types
type PatternVarOut a Source #
Methods
patternVars :: a -> [Arg (Either (PatternVarOut a) Term)] Source #
Instances
| PatternVars (Arg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (Arg (Pattern' a)) Source # | |
| PatternVars (NamedArg (Pattern' a)) Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut (NamedArg (Pattern' a)) Source # | |
| PatternVars a => PatternVars [a] Source # | |
Defined in Agda.Syntax.Internal Associated Types type PatternVarOut [a] Source # Methods patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)] Source # | |
data EqualityView Source #
View type as equality type.
Constructors
| EqualityViewType EqualityTypeData | |
| OtherType Type | reduced |
| IdiomType Type | reduced |
Instances
data EqualityTypeData Source #
Constructors
| EqualityTypeData | |
Instances
| EqualityUnview EqualityTypeData Source # | |
Defined in Agda.TypeChecking.Monad.Builtin Methods | |
| Subst EqualityTypeData Source # | |
Defined in Agda.TypeChecking.Substitute Associated Types type SubstArg EqualityTypeData Source # Methods applySubst :: Substitution' (SubstArg EqualityTypeData) -> EqualityTypeData -> EqualityTypeData Source # | |
| type SubstArg EqualityTypeData Source # | |
Defined in Agda.TypeChecking.Substitute | |
View type as path type.
data IntervalView Source #
Constructors
| IZero | |
| IOne | |
| IMin (Arg Term) (Arg Term) | |
| IMax (Arg Term) (Arg Term) | |
| INeg (Arg Term) | |
| OTerm Term |
Instances
| Show IntervalView Source # | |
Defined in Agda.Syntax.Internal Methods showsPrec :: Int -> IntervalView -> ShowS # show :: IntervalView -> String # showList :: [IntervalView] -> ShowS # | |
type DummyTermKind = String Source #
Constructing a singleton telescope.
class Suggest a where Source #
Suggest a name if available (i.e. name is not "_")
Methods
suggestName :: a -> Maybe String Source #
Instances
| Suggest Name Source # | |
Defined in Agda.Syntax.Internal | |
| Suggest Term Source # | |
Defined in Agda.Syntax.Internal | |
| Suggest String Source # | |
Defined in Agda.Syntax.Internal | |
| Suggest (Abs b) Source # | |
Defined in Agda.Syntax.Internal | |
data Suggestion Source #
Constructors
| forall a.Suggest a => Suggestion a |
Instances
| type TypeOf Elims Source # | |
| type TypeOf Level Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf PlusLevel Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf Sort Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf Term Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf Type Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf NLPat Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
| type TypeOf (Arg a) Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf (Abs Term) Source # | |
| type TypeOf (Abs Type) Source # | |
| type TypeOf (Dom a) Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf [PlusLevel] Source # | |
Defined in Agda.Syntax.Internal | |
| type TypeOf [Elim' NLPat] Source # | |
pattern EqualityType :: Sort -> QName -> Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView Source #
pattern ClosedLevel :: Integer -> Level Source #
Constant level n
argFromDom :: Dom' t a -> Arg a Source #
namedArgFromDom :: Dom' t a -> NamedArg a Source #
domFromArg :: Arg a -> Dom a Source #
domFromNamedArg :: NamedArg a -> Dom a Source #
defaultDom :: a -> Dom a Source #
defaultArgDom :: ArgInfo -> a -> Dom a Source #
isStrictDataSort :: Sort' t -> Bool Source #
Is this a strict universe inhabitable by data types?
clausePats :: Clause -> [Arg DeBruijnPattern] Source #
nameToPatVarName :: Name -> PatVarName Source #
namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #
absurdP :: Int -> DeBruijnPattern Source #
Make an absurd pattern with the given de Bruijn index.
toConPatternInfo :: ConInfo -> ConPatternInfo Source #
Build partial ConPatternInfo from ConInfo
fromConPatternInfo :: ConPatternInfo -> ConInfo Source #
Build ConInfo from ConPatternInfo.
patternInfo :: Pattern' x -> Maybe PatternInfo Source #
Retrieve the PatternInfo from a pattern
properlyMatching :: Pattern' a -> Bool Source #
Does the pattern perform a match that could fail?
eqtSort :: EqualityView -> Sort Source #
eqtName :: EqualityView -> QName Source #
eqtParams :: EqualityView -> Args Source #
isEqualityType :: EqualityView -> Bool Source #
isPathType :: PathView -> Bool Source #
isIOne :: IntervalView -> Bool Source #
absurdBody :: Abs Term Source #
Absurd lambdas are internally represented as identity with variable name "()".
isAbsurdPatternName :: PatVarName -> Bool Source #
dummyLocName :: CallStack -> String Source #
Construct a string representing the call-site that created the dummy thing.
dummyTermWith :: DummyTermKind -> CallStack -> Term Source #
Aux: A dummy term to constitute a dummy termlevelsort/type.
dummyLevel :: CallStack -> Level Source #
A dummy level to constitute a level/sort created at location. Note: use macro DUMMY_LEVEL !
atomicLevel :: t -> Level' t Source #
dummyTerm :: CallStack -> Term Source #
A dummy term created at location. Note: use macro DUMMY_TERM !
__DUMMY_TERM__ :: HasCallStack => Term Source #
__DUMMY_LEVEL__ :: HasCallStack => Level Source #
dummySort :: CallStack -> Sort Source #
A dummy sort created at location. Note: use macro DUMMY_SORT !
__DUMMY_SORT__ :: HasCallStack => Sort Source #
dummyType :: CallStack -> Type Source #
A dummy type created at location. Note: use macro DUMMY_TYPE !
__DUMMY_TYPE__ :: HasCallStack => Type Source #
dummyDom :: CallStack -> Dom Type Source #
Context entries without a type have this dummy type. Note: use macro DUMMY_DOM !
__DUMMY_DOM__ :: HasCallStack => Dom Type Source #
impossibleTerm :: CallStack -> Term Source #
mapAbsNamesM :: Applicative m => (ArgName -> m ArgName) -> Tele a -> m (Tele a) Source #
A traversal for the names in a telescope.
telFromList :: ListTel -> Telescope Source #
Convert a list telescope to a telescope.
suggests :: [Suggestion] -> String Source #
unSpine' :: (ProjOrigin -> QName -> Bool) -> Term -> Term Source #
Convert Proj projection eliminations
according to their ProjOrigin into
Def projection applications.
hasElims :: Term -> Maybe (Elims -> Term, Elims) Source #
A view distinguishing the neutrals Var, Def, and MetaV which
can be projected.
module Agda.Syntax.Internal.Elim
module Agda.Syntax.Internal.Univ
module Agda.Syntax.Abstract.Name
Meta-variable identifiers use the same structure as NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.