Agda.TypeChecking.Primitive.Cubical

Documentation

requireCubical

Arguments

:: Cubical

Which variant of Cubical Agda is required?

-> String

-> TCM ()

Checks that the correct variant of Cubical Agda is activated. Note that --erased-cubical "counts as" --cubical in erased contexts.

primIntervalType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Type

primINeg' :: TCM PrimitiveImpl

primDepIMin' :: TCM PrimitiveImpl

primIBin :: IntervalView -> IntervalView -> TCM PrimitiveImpl

primIMin' :: TCM PrimitiveImpl

primIMax' :: TCM PrimitiveImpl

imax :: HasBuiltins m => m Term -> m Term -> m Term

imin :: HasBuiltins m => m Term -> m Term -> m Term

primIdJ :: TCM PrimitiveImpl

primIdElim' :: TCM PrimitiveImpl

primPOr :: TCM PrimitiveImpl

primPartial' :: TCM PrimitiveImpl

primPartialP' :: TCM PrimitiveImpl

primSubOut' :: TCM PrimitiveImpl

primIdFace' :: TCM PrimitiveImpl

primIdPath' :: TCM PrimitiveImpl

primTrans' :: TCM PrimitiveImpl

primHComp' :: TCM PrimitiveImpl

data TranspOrHComp

Constructors

DoTransp

DoHComp

Instances

Show TranspOrHComp

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> TranspOrHComp -> ShowS

show :: TranspOrHComp -> String

showList :: [TranspOrHComp] -> ShowS

Eq TranspOrHComp

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

(==) :: TranspOrHComp -> TranspOrHComp -> Bool

(/=) :: TranspOrHComp -> TranspOrHComp -> Bool

cmdToName :: TranspOrHComp -> String

data FamilyOrNot a

Constructors

IsFam

Fields

• famThing :: a

IsNot

Fields

• famThing :: a

Instances

Foldable FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

fold :: Monoid m => FamilyOrNot m -> m

foldMap :: Monoid m => (a -> m) -> FamilyOrNot a -> m

foldMap' :: Monoid m => (a -> m) -> FamilyOrNot a -> m

foldr :: (a -> b -> b) -> b -> FamilyOrNot a -> b

foldr' :: (a -> b -> b) -> b -> FamilyOrNot a -> b

foldl :: (b -> a -> b) -> b -> FamilyOrNot a -> b

foldl' :: (b -> a -> b) -> b -> FamilyOrNot a -> b

foldr1 :: (a -> a -> a) -> FamilyOrNot a -> a

foldl1 :: (a -> a -> a) -> FamilyOrNot a -> a

toList :: FamilyOrNot a -> [a]

null :: FamilyOrNot a -> Bool

length :: FamilyOrNot a -> Int

elem :: Eq a => a -> FamilyOrNot a -> Bool

maximum :: Ord a => FamilyOrNot a -> a

minimum :: Ord a => FamilyOrNot a -> a

sum :: Num a => FamilyOrNot a -> a

product :: Num a => FamilyOrNot a -> a

Traversable FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

traverse :: Applicative f => (a -> f b) -> FamilyOrNot a -> f (FamilyOrNot b)

sequenceA :: Applicative f => FamilyOrNot (f a) -> f (FamilyOrNot a)

mapM :: Monad m => (a -> m b) -> FamilyOrNot a -> m (FamilyOrNot b)

sequence :: Monad m => FamilyOrNot (m a) -> m (FamilyOrNot a)

Functor FamilyOrNot

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b

(<$) :: a -> FamilyOrNot b -> FamilyOrNot a

Reduce a => Reduce (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a)

reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a))

Show a => Show (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> FamilyOrNot a -> ShowS

show :: FamilyOrNot a -> String

showList :: [FamilyOrNot a] -> ShowS

Eq a => Eq (FamilyOrNot a)

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

(==) :: FamilyOrNot a -> FamilyOrNot a -> Bool

(/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool

mkGComp :: HasBuiltins m => String -> NamesT m (NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term -> NamesT m Term)

Define a "ghcomp" version of gcomp. Normal comp looks like:

comp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u ] (forward A 0 u0)

So for "gcomp" we compute:

gcomp^i A [ phi -> u ] u0 = hcomp^i A(1/i) [ phi -> forward A i u, ~ phi -> forward A 0 u0 ] (forward A 0 u0)

The point of this is that gcomp does not produce any empty systems (if phi = 0 it will reduce to "forward A 0 u".

unglueTranspGlue :: PureTCM m => Arg Term -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> m Term

data TermPosition

Constructors

Head

Eliminated

Instances

Show TermPosition

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> TermPosition -> ShowS

show :: TermPosition -> String

showList :: [TermPosition] -> ShowS

Eq TermPosition

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

(==) :: TermPosition -> TermPosition -> Bool

(/=) :: TermPosition -> TermPosition -> Bool

headStop :: PureTCM m => TermPosition -> m Term -> m Bool

compGlue :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)

compHCompU :: PureTCM m => TranspOrHComp -> Arg Term -> Maybe (Arg Term) -> Arg Term -> FamilyOrNot (Arg Term, Arg Term, Arg Term, Arg Term) -> TermPosition -> m (Maybe Term)

primTransHComp :: TranspOrHComp -> [Arg Term] -> Int -> ReduceM (Reduced MaybeReducedArgs Term)

primComp :: TCM PrimitiveImpl

prim_glueU' :: TCM PrimitiveImpl

prim_unglueU' :: TCM PrimitiveImpl

primGlue' :: TCM PrimitiveImpl

prim_glue' :: TCM PrimitiveImpl

prim_unglue' :: TCM PrimitiveImpl

primFaceForall' :: TCM PrimitiveImpl

decomposeInterval :: HasBuiltins m => Term -> m [(Map Int Bool, [Term])]

decomposeInterval' :: HasBuiltins m => Term -> m [(Map Int (Set Bool), [Term])]

transpTel :: Abs Telescope -> Term -> Args -> ExceptT (Closure (Abs Type)) TCM Args

Tries to primTransp a whole telescope of arguments, following the rule for Σ types. If a type in the telescope does not support transp, transpTel throws it as an exception.

trFillTel :: Abs Telescope -> Term -> Args -> Term -> ExceptT (Closure (Abs Type)) TCM Args

Like transpTel but performing a transpFill.