Eq TranspOrHComp Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: TranspOrHComp -> TranspOrHComp -> Bool # (/=) :: TranspOrHComp -> TranspOrHComp -> Bool #
Show TranspOrHComp Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TranspOrHComp -> ShowS # show :: TranspOrHComp -> String # showList :: [TranspOrHComp] -> ShowS #

cmdToName :: TranspOrHComp -> String Source #

data FamilyOrNot a Source #

Constructors

IsFam
Fields famThing :: a
IsNot
Fields famThing :: a

Instances

Instances details

Functor FamilyOrNot Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods fmap :: (a -> b) -> FamilyOrNot a -> FamilyOrNot b # (<$) :: a -> FamilyOrNot b -> FamilyOrNot a #
Foldable FamilyOrNot Source #
Instance details 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 Source #
Instance details 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) #
Eq a => Eq (FamilyOrNot a) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: FamilyOrNot a -> FamilyOrNot a -> Bool # (/=) :: FamilyOrNot a -> FamilyOrNot a -> Bool #
Show a => Show (FamilyOrNot a) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> FamilyOrNot a -> ShowS # show :: FamilyOrNot a -> String # showList :: [FamilyOrNot a] -> ShowS #
Reduce a => Reduce (FamilyOrNot a) Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods reduce' :: FamilyOrNot a -> ReduceM (FamilyOrNot a) Source # reduceB' :: FamilyOrNot a -> ReduceM (Blocked (FamilyOrNot a)) Source #

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

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 Source #

data TermPosition Source #

Constructors

Head
Eliminated

Instances

Instances details

Eq TermPosition Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods (==) :: TermPosition -> TermPosition -> Bool # (/=) :: TermPosition -> TermPosition -> Bool #
Show TermPosition Source #
Instance details Defined in Agda.TypeChecking.Primitive.Cubical Methods showsPrec :: Int -> TermPosition -> ShowS # show :: TermPosition -> String # showList :: [TermPosition] -> ShowS #

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

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) Source #

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

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

primComp :: TCM PrimitiveImpl Source #

prim_glueU' :: TCM PrimitiveImpl Source #

prim_unglueU' :: TCM PrimitiveImpl Source #

primGlue' :: TCM PrimitiveImpl Source #

prim_glue' :: TCM PrimitiveImpl Source #

prim_unglue' :: TCM PrimitiveImpl Source #

primFaceForall' :: TCM PrimitiveImpl Source #

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

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

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

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 Source #

Like transpTel but performing a transpFill.