Abstractions

Methods

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

(Subst a, EqualSy a) => EqualSy (Abs a) Source #

Ignores absName.

Instance details

Methods

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

Free t => Free (Abs t) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Generic

Methods

freeVars :: ComputeFree r => Abs t -> Reader r (Collect r) Source #

PrecomputeFreeVars a => PrecomputeFreeVars (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Abs a -> FV (Abs a) Source #

(Reduce a, ForceNotFree a) => ForceNotFree (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Reduce

Methods

forceNotFree' :: Abs a -> FreeRed (Abs a)

MentionsMeta t => MentionsMeta (Abs t) Source #

Instance details

Defined in Mikan.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Abs t -> Bool Source #

UnFreezeMeta a => UnFreezeMeta (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Monad.MetaVars

Methods

unfreezeMeta :: MonadMetaSolver m => Abs a -> m () Source #

(PrettyTCM a, Subst a) => PrettyTCM (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Abs a -> m Doc Source #

Instantiate t => Instantiate (Abs t) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiate' :: Abs t -> ReduceM (Abs t) Source #

(Subst a, InstantiateFull a) => InstantiateFull (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Abs a -> ReduceM (Abs a) Source #

(Subst a, Normalise a) => Normalise (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: Abs a -> ReduceM (Abs a) Source #

(Subst a, Reduce a) => Reduce (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: Abs a -> ReduceM (Abs a) Source #

reduceB' :: Abs a -> ReduceM (Blocked (Abs a)) Source #

(Subst a, Simplify a) => Simplify (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

simplify' :: Abs a -> ReduceM (Abs a)

EmbPrj a => EmbPrj (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Abs a -> S Word32 Source #

icod_ :: Abs a -> S Word32 Source #

value :: Word32 -> R (Abs a) Source #

Subst a => Subst (Abs a) Source #

Instance details

Associated Types

type SubstArg (Abs a)
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg (Abs a) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Abs a)) -> Abs a -> Abs a Source #

(Subst a, SynEq a) => SynEq (Abs a) Source #

Instance details

Defined in Mikan.TypeChecking.SyntacticEquality

Methods

synEq :: Abs a -> Abs a -> SynEqA (Abs a)

Sized a => Sized (Abs a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

size :: Abs a -> Int Source #

natSize :: Abs a -> Peano Source #

NFData a => NFData (Abs a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

rnf :: Abs a -> () #

Generic (Abs a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Associated Types

type Rep (Abs a)

Instance details

Defined in Mikan.Syntax.Internal.Dom

type Rep (Abs a) = D1 ('MetaData "Abs" "Mikan.Syntax.Internal.Dom" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

Methods

from :: Abs a -> Rep (Abs a) x #

to :: Rep (Abs a) x -> Abs a #

Show a => Show (Abs a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

showsPrec :: Int -> Abs a -> ShowS #

show :: Abs a -> String #

showList :: [Abs a] -> ShowS #

(Subst a, Eq a) => Eq (Abs a) Source #

Equality of binders relies on weakening which is a special case of renaming which is a special case of substitution.

Instance details

Methods

(==) :: Abs a -> Abs a -> Bool #

(/=) :: Abs a -> Abs a -> Bool #

(Subst a, Ord a) => Ord (Abs a) Source #

Instance details

Methods

compare :: Abs a -> Abs a -> Ordering #

(<) :: Abs a -> Abs a -> Bool #

(<=) :: Abs a -> Abs a -> Bool #

(>) :: Abs a -> Abs a -> Bool #

(>=) :: Abs a -> Abs a -> Bool #

max :: Abs a -> Abs a -> Abs a #

min :: Abs a -> Abs a -> Abs a #

type TypeOf (Abs Term) Source #

Instance details

type TypeOf (Abs Term) = (Dom Type, Abs Type)

type TypeOf (Abs Type) Source #

Instance details

type TypeOf (Abs Type) = Dom Type

type ReifiesTo (Abs i) Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo (Abs i) = (Name, ReifiesTo i)

type SubstArg (Abs a) Source #

Instance details

type SubstArg (Abs a) = SubstArg a

type Rep (Abs a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

type Rep (Abs a) = D1 ('MetaData "Abs" "Mikan.Syntax.Internal.Dom" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Abs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "NoAbs" 'PrefixI 'True) (S1 ('MetaSel ('Just "absName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ArgName) :*: S1 ('MetaSel ('Just "unAbs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

isAbs :: Abs a -> Bool Source #

Domains

data DomInfo t Source #

Constructors

DomInfo
Fields domInfoArgInfo :: !ArgInfo domInfoName :: !(Maybe NamedName) e.g. `x` in `{x = y : A} -> B`. domInfoIsFinite :: !Bool Is this a Π-type (False), or a partial type (True)? domInfoTactic :: !(Maybe t) "@tactic e".

Instances

Instances details

Show t => Show (DomInfo t) Source #
Instance details Defined in Mikan.Syntax.Internal.Dom Methods showsPrec :: Int -> DomInfo t -> ShowS # show :: DomInfo t -> String # showList :: [DomInfo t] -> ShowS #
Eq (DomInfo Term) Source #
Instance details Defined in Mikan.TypeChecking.Substitute Methods (==) :: DomInfo Term -> DomInfo Term -> Bool # (/=) :: DomInfo Term -> DomInfo Term -> Bool #
Ord (DomInfo Term) Source #
Instance details Defined in Mikan.TypeChecking.Substitute Methods compare :: DomInfo Term -> DomInfo Term -> Ordering # (<) :: DomInfo Term -> DomInfo Term -> Bool # (<=) :: DomInfo Term -> DomInfo Term -> Bool # (>) :: DomInfo Term -> DomInfo Term -> Bool # (>=) :: DomInfo Term -> DomInfo Term -> Bool # max :: DomInfo Term -> DomInfo Term -> DomInfo Term # min :: DomInfo Term -> DomInfo Term -> DomInfo Term #

data Dom' t e Source #

Similar to Arg, but for domain types of functions and telescopes.

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) = True for the domain of a Pi type, 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'
Fields domDomInfo :: !(DomInfo t) unDom :: e

Bundled Patterns

pattern Dom :: ArgInfo -> Maybe NamedName -> Bool -> Maybe t -> e -> Dom' t e

Instances

Instances details

GetDefs Telescope Source #

Instance details

Defined in Mikan.Syntax.Internal.Defs

Methods

getDefs :: (Monoid m, ExpandCase LiftedRep m) => (MetaId -> Maybe Term) -> (QName -> m) -> Telescope -> m Source #

Reify Telescope Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo Telescope
Instance details Defined in Mikan.Syntax.Translation.InternalToAbstract type ReifiesTo Telescope = Telescope

Methods

reify :: MonadReify m => Telescope -> m (ReifiesTo Telescope) Source #

reifyWhen :: MonadReify m => Bool -> Telescope -> m (ReifiesTo Telescope) Source #

DropArgs Telescope Source #

NOTE: This creates telescopes with unbound de Bruijn indices.

Instance details

Defined in Mikan.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Telescope -> Telescope Source #

AddContext Telescope Source #

Instance details

Methods

addContext :: MonadAddContext m => Telescope -> m a -> m a Source #

PrettyTCM Telescope Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Telescope -> m Doc Source #

Reduce Telescope Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: Telescope -> ReduceM Telescope Source #

reduceB' :: Telescope -> ReduceM (Blocked Telescope) Source #

TeleNoAbs ListTel Source #

Instance details

Methods

teleNoAbs :: ListTel -> Term -> Term Source #

TeleNoAbs Telescope Source #

Instance details

Methods

teleNoAbs :: Telescope -> Term -> Term Source #

Abstract Telescope Source #

Instance details

Methods

abstract :: Telescope -> Telescope -> Telescope Source #

GetDefs a => GetDefs (Dom a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Defs

Methods

getDefs :: (Monoid m, ExpandCase LiftedRep m) => (MetaId -> Maybe Term) -> (QName -> m) -> Dom a -> m Source #

LensSort a => LensSort (Dom a) Source #

Instance details

Methods

lensSort :: Lens' (Dom a) Sort Source #

getSort :: Dom a -> Sort Source #

Reify i => Reify (Dom i) Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (Dom i)
Instance details Defined in Mikan.Syntax.Translation.InternalToAbstract type ReifiesTo (Dom i) = Arg (ReifiesTo i)

Methods

reify :: MonadReify m => Dom i -> m (ReifiesTo (Dom i)) Source #

reifyWhen :: MonadReify m => Bool -> Dom i -> m (ReifiesTo (Dom i)) Source #

AbsTerm a => AbsTerm (Dom a) Source #

Instance details

Methods

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

EqualSy a => EqualSy (Dom a) Source #

Ignore the tactic.

Instance details

Methods

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

Free t => Free (Dom t) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Generic

Methods

freeVars :: ComputeFree r => Dom t -> Reader r (Collect r) Source #

PrecomputeFreeVars a => PrecomputeFreeVars (Dom a) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Precompute

Methods

precomputeFreeVars :: Dom a -> FV (Dom a) Source #

(Reduce a, ForceNotFree a, TermSubst a) => ForceNotFree (Dom a) Source #

Instance details

Defined in Mikan.TypeChecking.Free.Reduce

Methods

forceNotFree' :: Dom a -> FreeRed (Dom a)

MentionsMeta t => MentionsMeta (Dom t) Source #

Instance details

Defined in Mikan.TypeChecking.MetaVars.Mention

Methods

mentionsMetas :: HashSet MetaId -> Dom t -> Bool Source #

AddContext (KeepNames Telescope) Source #

Instance details

Methods

addContext :: MonadAddContext m => KeepNames Telescope -> m a -> m a Source #

PrettyTCM (Dom Type) Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Dom Type -> m Doc Source #

ToTerm (Dom Type) Source #

Instance details

Defined in Mikan.TypeChecking.Primitive

Methods

toTerm :: TCM (Dom Type -> ReduceM Term) Source #

Instantiate e => Instantiate (Dom e) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiate' :: Dom e -> ReduceM (Dom e) Source #

InstantiateFull e => InstantiateFull (Dom e) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Dom e -> ReduceM (Dom e) Source #

Normalise t => Normalise (Dom t) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: Dom t -> ReduceM (Dom t) Source #

Reduce t => Reduce (Dom t) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: Dom t -> ReduceM (Dom t) Source #

reduceB' :: Dom t -> ReduceM (Blocked (Dom t)) Source #

Simplify t => Simplify (Dom t) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

simplify' :: Dom t -> ReduceM (Dom t)

EmbPrj a => EmbPrj (Dom a) Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Dom a -> S Word32 Source #

icod_ :: Dom a -> S Word32 Source #

value :: Word32 -> R (Dom a) Source #

SynEq a => SynEq (Dom a) Source #

Ignores tactic argument annotations.

Instance details

Defined in Mikan.TypeChecking.SyntacticEquality

Methods

synEq :: Dom a -> Dom a -> SynEqA (Dom a)

Unquote a => Unquote (Dom a) Source #

Instance details

Defined in Mikan.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Dom a) Source #

Decoration (Dom' t) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

traverseF :: Functor m => (a -> m b) -> Dom' t a -> m (Dom' t b) Source #

distributeF :: Functor m => Dom' t (m a) -> m (Dom' t a) Source #

Functor (Dom' t) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

fmap :: (a -> b) -> Dom' t a -> Dom' t b #

(<$) :: a -> Dom' t b -> Dom' t a #

Foldable (Dom' t) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

fold :: Monoid m => Dom' t m -> m #

foldMap :: Monoid m => (a -> m) -> Dom' t a -> m #

foldMap' :: Monoid m => (a -> m) -> Dom' t a -> m #

foldr :: (a -> b -> b) -> b -> Dom' t a -> b #

foldr' :: (a -> b -> b) -> b -> Dom' t a -> b #

foldl :: (b -> a -> b) -> b -> Dom' t a -> b #

foldl' :: (b -> a -> b) -> b -> Dom' t a -> b #

foldr1 :: (a -> a -> a) -> Dom' t a -> a #

foldl1 :: (a -> a -> a) -> Dom' t a -> a #

toList :: Dom' t a -> [a] #

null :: Dom' t a -> Bool #

length :: Dom' t a -> Int #

elem :: Eq a => a -> Dom' t a -> Bool #

maximum :: Ord a => Dom' t a -> a #

minimum :: Ord a => Dom' t a -> a #

sum :: Num a => Dom' t a -> a #

product :: Num a => Dom' t a -> a #

Traversable (Dom' t) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

traverse :: Applicative f => (a -> f b) -> Dom' t a -> f (Dom' t b) #

sequenceA :: Applicative f => Dom' t (f a) -> f (Dom' t a) #

mapM :: Monad m => (a -> m b) -> Dom' t a -> m (Dom' t b) #

sequence :: Monad m => Dom' t (m a) -> m (Dom' t a) #

Ord a => Ord (Dom a) Source #

Instance details

Methods

compare :: Dom a -> Dom a -> Ordering #

(<) :: Dom a -> Dom a -> Bool #

(<=) :: Dom a -> Dom a -> Bool #

(>) :: Dom a -> Dom a -> Bool #

(>=) :: Dom a -> Dom a -> Bool #

max :: Dom a -> Dom a -> Dom a #

min :: Dom a -> Dom a -> Dom a #

LensArgInfo (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

getArgInfo :: Dom' t e -> ArgInfo Source #

setArgInfo :: ArgInfo -> Dom' t e -> Dom' t e Source #

mapArgInfo :: (ArgInfo -> ArgInfo) -> Dom' t e -> Dom' t e Source #

LensFreeVariables (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

getFreeVariables :: Dom' t e -> FreeVariables Source #

setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source #

mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e Source #

LensHiding (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

getHiding :: Dom' t e -> Hiding Source #

setHiding :: Hiding -> Dom' t e -> Dom' t e Source #

mapHiding :: (Hiding -> Hiding) -> Dom' t e -> Dom' t e Source #

LensNamed (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Associated Types

type NameOf (Dom' t e)
Instance details Defined in Mikan.Syntax.Internal.Dom type NameOf (Dom' t e) = NamedName

Methods

lensNamed :: Lens' (Dom' t e) (Maybe (NameOf (Dom' t e))) Source #

LensOrigin (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

getOrigin :: Dom' t e -> Origin Source #

setOrigin :: Origin -> Dom' t e -> Dom' t e Source #

mapOrigin :: (Origin -> Origin) -> Dom' t e -> Dom' t e Source #

(Pretty t, Pretty e) => Pretty (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

pretty :: Dom' t e -> Doc Source #

prettyPrec :: Int -> Dom' t e -> Doc Source #

prettyList :: [Dom' t e] -> Doc Source #

(TermLike a, TermLike b) => TermLike (Dom' a b) Source #

Instance details

Defined in Mikan.Syntax.Internal.Generic

Methods

traverseTermM :: Monad m => (Term -> m Term) -> Dom' a b -> m (Dom' a b) Source #

foldTerm :: Monoid m => (Term -> m) -> Dom' a b -> m Source #

(AllMetas a, AllMetas b) => AllMetas (Dom' a b) Source #

Instance details

Defined in Mikan.Syntax.Internal.MetaVars

Methods

allMetas :: Monoid m => (MetaId -> m) -> Dom' a b -> m Source #

(NamesIn a, NamesIn b) => NamesIn (Dom' a b) Source #

Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Dom' a b -> m Source #

HasRange a => HasRange (Dom' t a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

getRange :: Dom' t a -> Range Source #

(KillRange t, KillRange a) => KillRange (Dom' t a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

killRange :: KillRangeT (Dom' t a) Source #

(ToAbstract r, AbsOfRef r ~ Expr) => ToAbstract (Dom r, Name) Source #

Instance details

Defined in Mikan.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Dom r, Name)
Instance details Defined in Mikan.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Dom r, Name) = TypedBinding

Methods

toAbstract :: MonadReflectedToAbstract m => (Dom r, Name) -> m (AbsOfRef (Dom r, Name)) Source #

t ~ Term => AddContext (Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom' t Type -> m a -> m a Source #

t ~ Term => AddContext (Dom' t (Name, Type)) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom' t (Name, Type) -> m a -> m a Source #

t ~ Term => AddContext (Dom' t (ShortText, Type)) Source #

Instance details

Methods

addContext :: MonadAddContext m => Dom' t (ShortText, Type) -> m a -> m a Source #

t ~ Term => AddContext (Name, Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (Name, Dom' t Type) -> m a -> m a Source #

t ~ Term => AddContext (KeepNames ShortText, Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (KeepNames ShortText, Dom' t Type) -> m a -> m a Source #

t ~ Term => AddContext (List1 Name, Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (List1 Name, Dom' t Type) -> m a -> m a Source #

AddContext (List1 (WithHiding Name), Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source #

t ~ Term => AddContext (List1 (Dom' t Name), Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (List1 (Dom' t Name), Type) -> m a -> m a Source #

t ~ Term => AddContext (ShortText, Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => (ShortText, Dom' t Type) -> m a -> m a Source #

t ~ Term => AddContext ([Name], Dom' t Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => ([Name], Dom' t Type) -> m a -> m a Source #

AddContext ([WithHiding Name], Dom Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source #

t ~ Term => AddContext ([Dom' t Name], Type) Source #

Instance details

Methods

addContext :: MonadAddContext m => ([Dom' t Name], Type) -> m a -> m a Source #

(Subst a, Subst b, SubstArg a ~ SubstArg b) => Subst (Dom' a b) Source #

Instance details

Associated Types

type SubstArg (Dom' a b)
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg (Dom' a b) = SubstArg a

Methods

applySubst :: Substitution' (SubstArg (Dom' a b)) -> Dom' a b -> Dom' a b Source #

(NFData t, NFData e) => NFData (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

rnf :: Dom' t e -> () #

(Show t, Show e) => Show (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

showsPrec :: Int -> Dom' t e -> ShowS #

show :: Dom' t e -> String #

showList :: [Dom' t e] -> ShowS #

Eq a => Eq (Dom' t a) Source #

Ignores Origin and FreeVariables and tactic.

Instance details

Defined in Mikan.Syntax.Internal.Dom

Methods

(==) :: Dom' t a -> Dom' t a -> Bool #

(/=) :: Dom' t a -> Dom' t a -> Bool #

type ReifiesTo Telescope Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo Telescope = Telescope

type TypeOf (Dom a) Source #

Instance details

type TypeOf (Dom a) = TypeOf a

type ReifiesTo (Dom i) Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo (Dom i) = Arg (ReifiesTo i)

type NameOf (Dom' t e) Source #

Instance details

Defined in Mikan.Syntax.Internal.Dom

type NameOf (Dom' t e) = NamedName

type AbsOfRef (Dom r, Name) Source #

Instance details

Defined in Mikan.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Dom r, Name) = TypedBinding

type SubstArg (Dom' a b) Source #

Instance details