Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Primitive.Cubical

Synopsis

Documentation

requireCubical Source #

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.

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

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

data FamilyOrNot a Source #

Constructors

IsFam 

Fields

IsNot 

Fields

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

Show a => Show (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Reduce a => Reduce (FamilyOrNot a) Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

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".

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.