| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.Syntax.Internal.Term
Synopsis
- data Term where
- dontCare :: Term -> Term
- stripDontCare :: Term -> Term
- var :: Nat -> Term
- unsharedVar :: Nat -> Elims -> Term
- varTable :: Array Term
- varTableSize :: Int
- data ConHead = ConHead {
- conName :: !QName
- conDataRecord :: !DataOrRecord
- conInductive :: !Induction
- conFields :: [QName]
- type ConInfo = ConOrigin
- class LensConName a where
- lensConName :: Lens' a QName
- getConName :: a -> QName
- setConName :: QName -> a -> a
- mapConName :: (QName -> QName) -> a -> a
- data DummyTermKind
- __DUMMY_TERM_WITH__ :: HasCallStack => String -> Term
- __DUMMY_TERM__ :: HasCallStack => Term
- impossibleTerm :: CallStack -> Term
- module Mikan.Syntax.Internal.Elim
- type Args = [Arg Term]
- type Elims = [Elim]
- type Elim = Elim' Term
- type NamedArgs = [NamedArg Term]
- type Args1 = List1 (Arg Term)
- type NamedArgs1 = List1 (NamedArg Term)
- data SpineHead = SpineHead !SpineHead'
- data SpineHead'
- unSpine :: Term -> Term
- hasElims :: Term -> Maybe (Elims -> Term, Elims)
- data Type'' t a = El {}
- type Type' a = Type'' Term a
- type Type = Type' Term
- __DUMMY_TYPE__ :: HasCallStack => Type
- type Dom = Dom' Term
- __DUMMY_DOM__ :: HasCallStack => Dom Type
- module Mikan.Syntax.Internal.Univ
- data Sort' t where
- Univ Univ (Level' t)
- Inf Univ !Integer
- LevelUniv
- IntervalUniv
- CofUniv
- PiSort (Dom' t t) (Sort' t) (Abs (Sort' t))
- FunSort (Sort' t) (Sort' t)
- UnivSort (Sort' t)
- MetaS !MetaId [Elim' t]
- DefS QName [Elim' t]
- DummyS String
- pattern Prop :: Level' t -> Sort' t
- pattern SSet :: Level' t -> Sort' t
- pattern Type :: Level' t -> Sort' t
- type Sort = Sort' Term
- data UnivSize
- varSort :: Int -> Sort
- mkType :: Integer -> Sort
- mkProp :: Integer -> Sort
- mkSSet :: Integer -> Sort
- tmSort :: Term -> Sort
- tmSSort :: Term -> Sort
- isProp :: Sort' t -> Bool
- isStrictDataSort :: Sort' t -> Bool
- propToType :: Sort' t -> Sort' t
- isSort :: Term -> Maybe Sort
- sortUniv :: Sort' t -> Maybe Univ
- class LensSort a where
- __DUMMY_SORT__ :: HasCallStack => Sort
- data Level' t where
- Max !Integer [PlusLevel' t]
- pattern ClosedLevel :: Integer -> Level
- type Level = Level' Term
- data PlusLevel' t = Plus !Integer t
- type PlusLevel = PlusLevel' Term
- type LevelAtom = Term
- levelSuc :: Level -> Level
- levelPlus :: Integer -> Level -> Level
- atomicLevel :: t -> Level' t
- __DUMMY_LEVEL__ :: HasCallStack => Level
- data Substitution' a
- = IdS
- | EmptyS Impossible
- | a :# !(Substitution' a)
- | Strengthen Impossible !Int !(Substitution' a)
- | Wk !Int !(Substitution' a)
- | Lift !Int !(Substitution' a)
- type Substitution = Substitution' Term
- type Renaming = Substitution' Nat
- newtype NoSubst t a = NoSubst {
- unNoSubst :: a
- newtype BraveTerm = BraveTerm {}
- module Mikan.Syntax.Internal.Blockers
- type Blocked = Blocked' Term
- type NotBlocked = NotBlocked' Term
- type Blocked_ = Blocked ()
- class TermSize a where
- type family TypeOf a
- module Mikan.Syntax.Abstract.Name
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- newtype ProblemId = ProblemId Word64
Terms
A Term in internal syntax.
Mikan's internal syntax represents terms in beta-normal form, meaning
that it is impossible to represent something like (λ x → x) t.
However, terms are not "delta"-normalised, and applications of
defined constants that may yet reduce can be represented by the Def
constructor.
Constructors
| Lam ArgInfo (Abs Term) | Lambda abstraction. The |
| Def QName Elims | Elimination of a defined name, which may be a redex. |
| Con ConHead ConInfo Elims | Application of a defined constructor. The If the constructor has a boundary, a |
| MetaV !MetaId Elims | Elimination from a metavariable. The metavariable may be open or solved, local or remote. |
| Pi (Dom Type) (Abs Type) | Dependent or non-dependent function type, controlled by the
|
| Lit Literal | Embedding of |
| Sort Sort | Embedding of |
| Level Level | Embedding of universe |
| DontCare Term | Terms containing irrelevant (i.e.
|
| Dummy DummyTermKind Elims | A (part of a) term or type which is only used for internal purposes. The The second field accumulates eliminations in case we apply a dummy term to more of them. Dummy terms should never be used in places where they can affect type checking, so syntactic checks are free to ignore the eliminations, which are only there to ease debugging when a dummy term incorrectly leaks into a relevant position. |
Bundled Patterns
| pattern Var :: Int -> Elims -> Term | Neutral elimnation of a variable in the context (represented by its de Bruijn index). Term variables with no eliminations are globally cached in a shared
compacted array, which allows them to be pointer-equal; this is the
|
Instances
Variable sharing
unsharedVar :: Nat -> Elims -> Term Source #
Create a neutral elimnation of a variable without going through the global variable cache.
The main use of unsharedVar is when you know statically
that a variable *must* have eliminations.
varTable :: Array Term Source #
A lifted array of globally-shared Term variables with no
eliminations.
Variables with de Bruijn index less than varTableSize should be
drawn from this table instead of constructed. This is handled
automatically by the Var pattern synonym and var smart
constructor.
varTableSize :: Int Source #
Constructors
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
| LensConName ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name | |||||
| CopatternMatchingAllowed ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name Methods | |||||
| Pretty ConHead Source # | |||||
| NamesIn ConHead Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| HasRange ConHead Source # | |||||
| KillRange ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name Methods | |||||
| SetRange ConHead Source # | |||||
| PrettyTCM ConHead Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| InstantiateFull ConHead Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj ConHead Source # | |||||
| NFData ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name | |||||
| Generic ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name Associated Types
| |||||
| Show ConHead Source # | |||||
| Eq ConHead Source # | |||||
| Ord ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name | |||||
| type Rep ConHead Source # | |||||
Defined in Mikan.Syntax.Abstract.Name type Rep ConHead = D1 ('MetaData "ConHead" "Mikan.Syntax.Abstract.Name" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ConHead" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conName") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 QName) :*: S1 ('MetaSel ('Just "conDataRecord") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 DataOrRecord)) :*: (S1 ('MetaSel ('Just "conInductive") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Induction) :*: S1 ('MetaSel ('Just "conFields") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [QName])))) | |||||
class LensConName a where Source #
Minimal complete definition
Nothing
Methods
lensConName :: Lens' a QName Source #
getConName :: a -> QName Source #
setConName :: QName -> a -> a Source #
mapConName :: (QName -> QName) -> a -> a Source #
Instances
| LensConName ConHead Source # | |
Defined in Mikan.Syntax.Abstract.Name | |
Dummies
data DummyTermKind Source #
Terms used for internal purposes
Constructors
| DummyNamed String | Generic dummy term, the Should not be used to convey actual information. |
| DummyBrave Term | Collects applications to a |
| DummyDisplay | An underscore in the right-hand side of a This renders as an underscore when reified but it has the property of matching arbitrary patterns in display form matching. Can be used to allow chaining display forms for projections into display forms for copies, when the parameters can't be reconstructed. |
Instances
| EmbPrj DummyTermKind Source # | |
| IsString DummyTermKind Source # | |
Defined in Mikan.Syntax.Internal.Term Methods fromString :: String -> DummyTermKind # | |
| Show DummyTermKind Source # | |
Defined in Mikan.Syntax.Internal.Term Methods showsPrec :: Int -> DummyTermKind -> ShowS # show :: DummyTermKind -> String # showList :: [DummyTermKind] -> ShowS # | |
__DUMMY_TERM_WITH__ :: HasCallStack => String -> Term Source #
__DUMMY_TERM__ :: HasCallStack => Term Source #
impossibleTerm :: CallStack -> Term Source #
Arguments and eliminations
module Mikan.Syntax.Internal.Elim
Spined forms
Constructors
| SpineHead !SpineHead' |
data SpineHead' Source #
Types
Instances
| Pretty Type Source # | |||||
| GetDefs Telescope Source # | |||||
| GetDefs Type Source # | |||||
| Reify Telescope Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| Reify Type Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| AbsTerm Type Source # | |||||
| EqualSy Type Source # | Ignores sorts. | ||||
| CheckInternal Type Source # | |||||
Defined in Mikan.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Type -> Comparison -> TypeOf Type -> TCM Type Source # checkInternal :: Type -> Comparison -> TypeOf Type -> TCM () Source # inferInternal' :: Action -> Type -> TCM Type Source # inferInternal :: Type -> TCM () Source # | |||||
| DropArgs Telescope Source # | NOTE: This creates telescopes with unbound de Bruijn indices. | ||||
| PrecomputeFreeVars Type Source # | |||||
Defined in Mikan.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Type -> FV Type Source # | |||||
| ForceNotFree Type Source # | |||||
Defined in Mikan.TypeChecking.Free.Reduce Methods forceNotFree' :: Type -> FreeRed Type | |||||
| MentionsMeta Type Source # | |||||
Defined in Mikan.TypeChecking.MetaVars.Mention | |||||
| AddContext Telescope Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Telescope -> m a -> m a Source # | |||||
| UnFreezeMeta Type Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Type -> m () Source # | |||||
| PrettyTCM Telescope Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM Type Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrimTerm Type Source # | |||||
| PrimType Type Source # | |||||
| ToTerm Type Source # | |||||
| Reduce Telescope Source # | |||||
| Reduce Type Source # | |||||
| TeleNoAbs ListTel Source # | |||||
| TeleNoAbs Telescope Source # | |||||
| Abstract Telescope Source # | |||||
| Abstract Type Source # | |||||
| SynEq Type Source # | Syntactic equality ignores sorts. | ||||
Defined in Mikan.TypeChecking.SyntacticEquality | |||||
| NFData Type Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| LensSort (Type' a) Source # | |||||
| Free t => Free (Type' t) Source # | |||||
Defined in Mikan.TypeChecking.Free.Generic | |||||
| AddContext (KeepNames Telescope) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source # | |||||
| PrettyTCM (Arg Type) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (Dom Type) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| ToTerm (Dom Type) Source # | |||||
| Instantiate t => Instantiate (Type' t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| InstantiateFull t => InstantiateFull (Type' t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Normalise t => Normalise (Type' t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Simplify t => Simplify (Type' t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj a => EmbPrj (Type' a) Source # | |||||
| Decoration (Type'' t) Source # | |||||
| Functor (Type'' t) Source # | |||||
| Foldable (Type'' t) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fold :: Monoid m => Type'' t m -> m # foldMap :: Monoid m => (a -> m) -> Type'' t a -> m # foldMap' :: Monoid m => (a -> m) -> Type'' t a -> m # foldr :: (a -> b -> b) -> b -> Type'' t a -> b # foldr' :: (a -> b -> b) -> b -> Type'' t a -> b # foldl :: (b -> a -> b) -> b -> Type'' t a -> b # foldl' :: (b -> a -> b) -> b -> Type'' t a -> b # foldr1 :: (a -> a -> a) -> Type'' t a -> a # foldl1 :: (a -> a -> a) -> Type'' t a -> a # elem :: Eq a => a -> Type'' t a -> Bool # maximum :: Ord a => Type'' t a -> a # minimum :: Ord a => Type'' t a -> a # | |||||
| Traversable (Type'' t) Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| Eq a => Eq (Type' a) Source # | Syntactic | ||||
| Ord a => Ord (Type' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| TermLike b => TermLike (Type'' a b) Source # | |||||
| (TermLike a, TermLike b) => AllMetas (Type'' a b) Source # | |||||
| (NamesIn a, NamesIn b) => NamesIn (Type'' a b) Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| (KillRange a, KillRange b) => KillRange (Type'' a b) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Type'' a b) Source # | |||||
| t ~ Term => AddContext (Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom' t Type -> m a -> m a Source # | |||||
| t ~ Term => AddContext (Dom' t (Name, Type)) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom' t (Name, Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (Dom' t (ShortText, Type)) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => Dom' t (ShortText, Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (Name, Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (Name, Dom' t Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (KeepNames ShortText, Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (KeepNames ShortText, Dom' t Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (List1 Name, Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 Name, Dom' t Type) -> m a -> m a Source # | |||||
| AddContext (List1 (Arg Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Arg Name), Type) -> m a -> m a Source # | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # | |||||
| AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (List1 (Dom' t Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (Dom' t Name), Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext (ShortText, Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (ShortText, Dom' t Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext ([Name], Dom' t Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Name], Dom' t Type) -> m a -> m a Source # | |||||
| AddContext ([Arg Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Arg Name], Type) -> m a -> m a Source # | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # | |||||
| t ~ Term => AddContext ([Dom' t Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([Dom' t Name], Type) -> m a -> m a Source # | |||||
| IsMeta a => IsMeta (Type'' t a) Source # | |||||
| (Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Type'' a b) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Type'' a b)) -> Type'' a b -> Type'' a b Source # | |||||
| (Show t, Show a) => Show (Type'' t a) Source # | |||||
| type TypeOf Type Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| type ReifiesTo Telescope Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type ReifiesTo Type Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type TypeOf (Abs Type) Source # | |||||
| type SubstArg (Type'' a b) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
__DUMMY_TYPE__ :: HasCallStack => Type Source #
Domains
__DUMMY_DOM__ :: HasCallStack => Dom Type Source #
Sorts
module Mikan.Syntax.Internal.Univ
Sorts.
The three sort constructors MetaS, DefS and DummyS are the sort
equivalents of the term constructors Meta, Def and Dummy.
Constructors
| Univ Univ (Level' t) |
|
| Inf Univ !Integer |
|
| LevelUniv |
When |
| IntervalUniv |
|
| CofUniv |
|
| PiSort (Dom' t t) (Sort' t) (Abs (Sort' t)) | Sort of a pi type, as a function of the sort of its domain and the sort of its codomain (which may depend on the domain). |
| FunSort (Sort' t) (Sort' t) | Sort of a (non-dependent) function type. |
| UnivSort (Sort' t) | Sort of another sort. |
| MetaS !MetaId [Elim' t] | An unsolved sort metavariable. |
| DefS QName [Elim' t] | A postulated sort, used for unsolved sort metavariables left
open in a module checked with |
| DummyS String | A dummy sort, like a The |
Bundled Patterns
| pattern Prop :: Level' t -> Sort' t | |
| pattern SSet :: Level' t -> Sort' t | |
| pattern Type :: Level' t -> Sort' t |
Instances
| Pretty Sort Source # | |||||
| GetDefs Sort Source # | |||||
| TermLike Sort Source # | |||||
| AllMetas Sort Source # | |||||
| LensSort Sort Source # | |||||
| TermSize Sort Source # | |||||
| Reify Sort Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| AbsTerm Sort Source # | |||||
| EqualSy Sort Source # | |||||
| CheckInternal Sort Source # | |||||
Defined in Mikan.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Sort -> Comparison -> TypeOf Sort -> TCM Sort Source # checkInternal :: Sort -> Comparison -> TypeOf Sort -> TCM () Source # inferInternal' :: Action -> Sort -> TCM Sort Source # inferInternal :: Sort -> TCM () Source # | |||||
| Free Sort Source # | |||||
Defined in Mikan.TypeChecking.Free.Generic | |||||
| PrecomputeFreeVars Sort Source # | |||||
Defined in Mikan.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Sort -> FV Sort Source # | |||||
| ForceNotFree Sort Source # | |||||
Defined in Mikan.TypeChecking.Free.Reduce Methods forceNotFree' :: Sort -> FreeRed Sort | |||||
| MentionsMeta Sort Source # | |||||
Defined in Mikan.TypeChecking.MetaVars.Mention | |||||
| UnFreezeMeta Sort Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Sort -> m () Source # | |||||
| PrettyTCM Sort Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| Instantiate Sort Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| InstantiateFull Sort Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Normalise Sort Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Reduce Sort Source # | |||||
| Simplify Sort Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj Sort Source # | |||||
| Apply Sort Source # | |||||
| SynEq Sort Source # | |||||
Defined in Mikan.TypeChecking.SyntacticEquality | |||||
| NFData Sort Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| Eq Sort Source # | |||||
| Ord Sort Source # | |||||
| NamesIn a => NamesIn (Sort' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| KillRange a => KillRange (Sort' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Sort' a) Source # | |||||
| IsMeta (Sort' a) Source # | |||||
| Subst a => Subst (Sort' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Sort' a)) -> Sort' a -> Sort' a Source # | |||||
| Show t => Show (Sort' t) Source # | |||||
| type TypeOf Sort Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| type ReifiesTo Sort Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type SubstArg (Sort' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
isStrictDataSort :: Sort' t -> Bool Source #
Is this a strict universe inhabitable by data types?
propToType :: Sort' t -> Sort' t Source #
sortUniv :: Sort' t -> Maybe Univ Source #
Get the flavor of the universe. Nothing could also mean "don't know".
class LensSort a where Source #
Minimal complete definition
Nothing
Methods
__DUMMY_SORT__ :: HasCallStack => Sort Source #
Universe levels
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] |
Bundled Patterns
| pattern ClosedLevel :: Integer -> Level | Constant level |
Instances
| Pretty Level Source # | |||||
| GetDefs Level Source # | |||||
| TermLike Level Source # | |||||
| AllMetas Level Source # | |||||
| TermSize Level Source # | |||||
| Reify Level Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| AbsTerm Level Source # | |||||
| EqualSy Level Source # | |||||
| CheckInternal Level Source # | |||||
Defined in Mikan.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Level -> Comparison -> TypeOf Level -> TCM Level Source # checkInternal :: Level -> Comparison -> TypeOf Level -> TCM () Source # inferInternal' :: Action -> Level -> TCM Level Source # inferInternal :: Level -> TCM () Source # | |||||
| Free Level Source # | |||||
Defined in Mikan.TypeChecking.Free.Generic | |||||
| PrecomputeFreeVars Level Source # | |||||
Defined in Mikan.TypeChecking.Free.Precompute Methods precomputeFreeVars :: Level -> FV Level Source # | |||||
| ForceNotFree Level Source # | |||||
Defined in Mikan.TypeChecking.Free.Reduce Methods forceNotFree' :: Level -> FreeRed Level | |||||
| MentionsMeta Level Source # | |||||
Defined in Mikan.TypeChecking.MetaVars.Mention | |||||
| UnFreezeMeta Level Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => Level -> m () Source # | |||||
| PrettyTCM Level Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| Instantiate Level Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| InstantiateFull Level Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Normalise Level Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Reduce Level Source # | |||||
| Simplify Level Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj Level Source # | |||||
| DeBruijn Level Source # | |||||
Defined in Mikan.TypeChecking.Substitute.DeBruijn | |||||
| SynEq Level Source # | Returns levels in canonical form. | ||||
Defined in Mikan.TypeChecking.SyntacticEquality | |||||
| NFData Level Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| Functor Level' Source # | |||||
| Foldable Level' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fold :: Monoid m => Level' m -> m # foldMap :: Monoid m => (a -> m) -> Level' a -> m # foldMap' :: Monoid m => (a -> m) -> Level' a -> m # foldr :: (a -> b -> b) -> b -> Level' a -> b # foldr' :: (a -> b -> b) -> b -> Level' a -> b # foldl :: (b -> a -> b) -> b -> Level' a -> b # foldl' :: (b -> a -> b) -> b -> Level' a -> b # foldr1 :: (a -> a -> a) -> Level' a -> a # foldl1 :: (a -> a -> a) -> Level' a -> a # elem :: Eq a => a -> Level' a -> Bool # maximum :: Ord a => Level' a -> a # minimum :: Ord a => Level' a -> a # | |||||
| Traversable Level' Source # | |||||
| Eq Level Source # | |||||
| Ord Level Source # | |||||
| NamesIn a => NamesIn (Level' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| KillRange a => KillRange (Level' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (Level' a) Source # | |||||
| IsMeta a => IsMeta (Level' a) Source # | |||||
| Subst a => Subst (Level' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Level' a)) -> Level' a -> Level' a Source # | |||||
| Show t => Show (Level' t) Source # | |||||
| type TypeOf Level Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| type ReifiesTo Level Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type SubstArg (Level' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
data PlusLevel' t Source #
Instances
| Pretty PlusLevel Source # | |||||
| GetDefs PlusLevel Source # | |||||
| TermLike PlusLevel Source # | |||||
| AllMetas PlusLevel Source # | |||||
| TermSize PlusLevel Source # | |||||
| AbsTerm PlusLevel Source # | |||||
| EqualSy PlusLevel Source # | |||||
| CheckInternal PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.CheckInternal Methods checkInternal' :: Action -> PlusLevel -> Comparison -> TypeOf PlusLevel -> TCM PlusLevel Source # checkInternal :: PlusLevel -> Comparison -> TypeOf PlusLevel -> TCM () Source # inferInternal' :: Action -> PlusLevel -> TCM PlusLevel Source # inferInternal :: PlusLevel -> TCM () Source # | |||||
| PrecomputeFreeVars PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Free.Precompute Methods precomputeFreeVars :: PlusLevel -> FV PlusLevel Source # | |||||
| ForceNotFree PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Free.Reduce Methods forceNotFree' :: PlusLevel -> FreeRed PlusLevel | |||||
| MentionsMeta PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.MetaVars.Mention | |||||
| UnFreezeMeta PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => PlusLevel -> m () Source # | |||||
| InstantiateFull PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Normalise PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Reduce PlusLevel Source # | |||||
| Simplify PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj PlusLevel Source # | |||||
| DeBruijn PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.Substitute.DeBruijn | |||||
| SynEq PlusLevel Source # | |||||
Defined in Mikan.TypeChecking.SyntacticEquality | |||||
| NFData PlusLevel Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| Functor PlusLevel' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fmap :: (a -> b) -> PlusLevel' a -> PlusLevel' b # (<$) :: a -> PlusLevel' b -> PlusLevel' a # | |||||
| Foldable PlusLevel' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fold :: Monoid m => PlusLevel' m -> m # foldMap :: Monoid m => (a -> m) -> PlusLevel' a -> m # foldMap' :: Monoid m => (a -> m) -> PlusLevel' a -> m # foldr :: (a -> b -> b) -> b -> PlusLevel' a -> b # foldr' :: (a -> b -> b) -> b -> PlusLevel' a -> b # foldl :: (b -> a -> b) -> b -> PlusLevel' a -> b # foldl' :: (b -> a -> b) -> b -> PlusLevel' a -> b # foldr1 :: (a -> a -> a) -> PlusLevel' a -> a # foldl1 :: (a -> a -> a) -> PlusLevel' a -> a # toList :: PlusLevel' a -> [a] # null :: PlusLevel' a -> Bool # length :: PlusLevel' a -> Int # elem :: Eq a => a -> PlusLevel' a -> Bool # maximum :: Ord a => PlusLevel' a -> a # minimum :: Ord a => PlusLevel' a -> a # sum :: Num a => PlusLevel' a -> a # product :: Num a => PlusLevel' a -> a # | |||||
| Traversable PlusLevel' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods traverse :: Applicative f => (a -> f b) -> PlusLevel' a -> f (PlusLevel' b) # sequenceA :: Applicative f => PlusLevel' (f a) -> f (PlusLevel' a) # mapM :: Monad m => (a -> m b) -> PlusLevel' a -> m (PlusLevel' b) # sequence :: Monad m => PlusLevel' (m a) -> m (PlusLevel' a) # | |||||
| Eq PlusLevel Source # | |||||
| Ord PlusLevel Source # | |||||
| NamesIn a => NamesIn (PlusLevel' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> PlusLevel' a -> m Source # | |||||
| KillRange a => KillRange (PlusLevel' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods killRange :: KillRangeT (PlusLevel' a) Source # | |||||
| Free t => Free (PlusLevel' t) Source # | |||||
Defined in Mikan.TypeChecking.Free.Generic Methods freeVars :: ComputeFree r => PlusLevel' t -> Reader r (Collect r) Source # | |||||
| Instantiate t => Instantiate (PlusLevel' t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce Methods instantiate' :: PlusLevel' t -> ReduceM (PlusLevel' t) Source # | |||||
| IsMeta a => IsMeta (PlusLevel' a) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Subst a => Subst (PlusLevel' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (PlusLevel' a)) -> PlusLevel' a -> PlusLevel' a Source # | |||||
| Show t => Show (PlusLevel' t) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods showsPrec :: Int -> PlusLevel' t -> ShowS # show :: PlusLevel' t -> String # showList :: [PlusLevel' t] -> ShowS # | |||||
| type TypeOf PlusLevel Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| type TypeOf [PlusLevel] Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| type SubstArg (PlusLevel' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
type PlusLevel = PlusLevel' Term Source #
atomicLevel :: t -> Level' t Source #
__DUMMY_LEVEL__ :: HasCallStack => Level Source #
Substitutions
data Substitution' a Source #
Substitutions.
Constructors
| IdS | Identity substitution. Γ ⊢ IdS : Γ |
| EmptyS Impossible | Empty substitution, lifts from the empty context. Apply this to closed terms you want to use in a non-empty context. Γ ⊢ EmptyS : () The |
| a :# !(Substitution' a) infixr 4 | Substitution extension, "cons". Γ ⊢ u : Aρ Γ ⊢ ρ : Δ
---------------------
Γ ⊢ u :# ρ : Δ, A
|
| Strengthen Impossible !Int !(Substitution' a) | Strengthening substitution. In Γ ⊢ ρ : Δ |Θ| = n --------------------------- Γ ⊢ Strengthen n ρ : Δ, Θ The |
| Wk !Int !(Substitution' a) | Weakening substitution, lifts to an extended context. Γ ⊢ ρ : Δ ------------------- Γ, Ψ ⊢ Wk |Ψ| ρ : Δ |
| Lift !Int !(Substitution' a) | Lifting substitution. Use this to go under a binder.
Γ ⊢ ρ : Δ ------------------------- Γ, Ψρ ⊢ Lift |Ψ| ρ : Δ, Ψ |
Instances
| KillRange Substitution Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods | |||||
| InstantiateFull Substitution Source # | |||||
Defined in Mikan.TypeChecking.Reduce Methods instantiateFull' :: Substitution -> ReduceM Substitution Source # | |||||
| Functor Substitution' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fmap :: (a -> b) -> Substitution' a -> Substitution' b # (<$) :: a -> Substitution' b -> Substitution' a # | |||||
| Foldable Substitution' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods fold :: Monoid m => Substitution' m -> m # foldMap :: Monoid m => (a -> m) -> Substitution' a -> m # foldMap' :: Monoid m => (a -> m) -> Substitution' a -> m # foldr :: (a -> b -> b) -> b -> Substitution' a -> b # foldr' :: (a -> b -> b) -> b -> Substitution' a -> b # foldl :: (b -> a -> b) -> b -> Substitution' a -> b # foldl' :: (b -> a -> b) -> b -> Substitution' a -> b # foldr1 :: (a -> a -> a) -> Substitution' a -> a # foldl1 :: (a -> a -> a) -> Substitution' a -> a # toList :: Substitution' a -> [a] # null :: Substitution' a -> Bool # length :: Substitution' a -> Int # elem :: Eq a => a -> Substitution' a -> Bool # maximum :: Ord a => Substitution' a -> a # minimum :: Ord a => Substitution' a -> a # sum :: Num a => Substitution' a -> a # product :: Num a => Substitution' a -> a # | |||||
| Traversable Substitution' Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods traverse :: Applicative f => (a -> f b) -> Substitution' a -> f (Substitution' b) # sequenceA :: Applicative f => Substitution' (f a) -> f (Substitution' a) # mapM :: Monad m => (a -> m b) -> Substitution' a -> m (Substitution' b) # sequence :: Monad m => Substitution' (m a) -> m (Substitution' a) # | |||||
| Eq Substitution Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| Ord Substitution Source # | |||||
Defined in Mikan.TypeChecking.Substitute Methods compare :: Substitution -> Substitution -> Ordering # (<) :: Substitution -> Substitution -> Bool # (<=) :: Substitution -> Substitution -> Bool # (>) :: Substitution -> Substitution -> Bool # (>=) :: Substitution -> Substitution -> Bool # max :: Substitution -> Substitution -> Substitution # min :: Substitution -> Substitution -> Substitution # | |||||
| Pretty a => Pretty (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods pretty :: Substitution' a -> Doc Source # prettyPrec :: Int -> Substitution' a -> Doc Source # prettyList :: [Substitution' a] -> Doc Source # | |||||
| NamesIn a => NamesIn (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Substitution' a -> m Source # | |||||
| TermSize a => TermSize (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| (Pretty a, PrettyTCM a, EndoSubst a) => PrettyTCM (Substitution' a) Source # | |||||
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => Substitution' a -> m Doc Source # | |||||
| EmbPrj a => EmbPrj (Substitution' a) Source # | |||||
| EndoSubst a => Subst (Substitution' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Substitution' a)) -> Substitution' a -> Substitution' a Source # | |||||
| Null (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| NFData a => NFData (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods rnf :: Substitution' a -> () # | |||||
| Generic (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Associated Types
Methods from :: Substitution' a -> Rep (Substitution' a) x # to :: Rep (Substitution' a) x -> Substitution' a # | |||||
| Show a => Show (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Methods showsPrec :: Int -> Substitution' a -> ShowS # show :: Substitution' a -> String # showList :: [Substitution' a] -> ShowS # | |||||
| type SubstArg (Substitution' a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| type Rep (Substitution' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term type Rep (Substitution' a) = D1 ('MetaData "Substitution'" "Mikan.Syntax.Internal.Term" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "IdS" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "EmptyS" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible)) :+: C1 ('MetaCons ":#" ('InfixI 'RightAssociative 4) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Substitution' a))))) :+: (C1 ('MetaCons "Strengthen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Impossible) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Substitution' a)))) :+: (C1 ('MetaCons "Wk" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Substitution' a))) :+: C1 ('MetaCons "Lift" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (Substitution' a)))))) | |||||
type Substitution = Substitution' Term Source #
type Renaming = Substitution' Nat Source #
Wrapper for types that do not contain variables (so applying a substitution is the identity). Useful if you have a structure of types that support substitution mixed with types that don't and need to apply a substitution to the full structure.
Instances
| Functor (NoSubst t) Source # | |||||
| Pretty a => Pretty (NoSubst t a) Source # | |||||
| DeBruijn t => Subst (NoSubst t a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute.Class Associated Types
Methods applySubst :: Substitution' (SubstArg (NoSubst t a)) -> NoSubst t a -> NoSubst t a Source # | |||||
| NFData a => NFData (NoSubst t a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
| Generic (NoSubst t a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term Associated Types
| |||||
| type SubstArg (NoSubst t a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute.Class | |||||
| type Rep (NoSubst t a) Source # | |||||
Defined in Mikan.Syntax.Internal.Term | |||||
Newtype for terms that produce a dummy when applied to incompatible eliminations, instead of crashing.
Instances
| Apply BraveTerm Source # | |||||
| Subst BraveTerm Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg BraveTerm) -> BraveTerm -> BraveTerm Source # | |||||
| DeBruijn BraveTerm Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
| Show BraveTerm Source # | |||||
| type SubstArg BraveTerm Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
Blocked terms
type NotBlocked = NotBlocked' Term Source #
Basic traversals
class TermSize a where Source #
The size of a term is roughly the number of nodes in its syntax tree.
This number is only used for heuristics, so it does not need to be accurately computed. Things like sort annotations may be skipped.
Minimal complete definition
Instances
| type TypeOf Elims Source # | |
| type TypeOf Level Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf PlusLevel Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf Sort Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf Term Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf Type Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf (Arg a) Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf (Abs Term) Source # | |
| type TypeOf (Abs Type) Source # | |
| type TypeOf (Dom a) Source # | |
Defined in Mikan.Syntax.Internal.Term | |
| type TypeOf [PlusLevel] Source # | |
Defined in Mikan.Syntax.Internal.Term | |
Reexports
module Mikan.Syntax.Abstract.Name
Meta-variable identifiers use the same structure as NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
| EncodeTCM MetaId Source # | |||||
| Pretty MetaId Source # | |||||
| GetDefs MetaId Source # | |||||
| NamesIn MetaId Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| Reify MetaId Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| HasFresh MetaId Source # | |||||
| UnFreezeMeta MetaId Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |||||
| PrettyTCM MetaId Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| FromTerm MetaId Source # | |||||
Defined in Mikan.TypeChecking.Primitive | |||||
| PrimTerm MetaId Source # | |||||
| PrimType MetaId Source # | |||||
| ToTerm MetaId Source # | |||||
| EmbPrj MetaId Source # | |||||
| Unquote MetaId Source # | |||||
| ToJSON MetaId Source # | |||||
| NFData MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic MetaId Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
| Eq MetaId Source # | |||||
| Ord MetaId Source # | |||||
| Hashable MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Singleton MetaId MetaSet Source # | |||||
| InstantiateFull (Judgement MetaId) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| type ReifiesTo MetaId Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type Rep MetaId Source # | |||||
Defined in Mikan.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) | |||||
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
| EncodeTCM ProblemId Source # | |
| Pretty ProblemId Source # | |
| HasFresh ProblemId Source # | |
| PrettyTCM ProblemId Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| EmbPrj ProblemId Source # | |
| ToJSON ProblemId Source # | |
| NFData ProblemId Source # | |
Defined in Mikan.Syntax.Common | |
| Enum ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods succ :: ProblemId -> ProblemId # pred :: ProblemId -> ProblemId # fromEnum :: ProblemId -> Int # enumFrom :: ProblemId -> [ProblemId] # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] # | |
| Num ProblemId Source # | |
Defined in Mikan.Syntax.Common | |
| Integral ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId # rem :: ProblemId -> ProblemId -> ProblemId # div :: ProblemId -> ProblemId -> ProblemId # mod :: ProblemId -> ProblemId -> ProblemId # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # | |
| Real ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods toRational :: ProblemId -> Rational # | |
| Show ProblemId Source # | |
| Eq ProblemId Source # | |
| Ord ProblemId Source # | |