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

Agda.TypeChecking.Primitive.Cubical

Synopsis

Documentation

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

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

data TranspOrHComp Source #

Constructors

DoTransp 
DoHComp 

Instances

Instances details
Eq TranspOrHComp Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Show TranspOrHComp Source # 
Instance details

Defined in Agda.TypeChecking.Primitive.Cubical

Methods

showsPrec :: Int -> TranspOrHComp -> ShowS

show :: TranspOrHComp -> String

showList :: [TranspOrHComp] -> ShowS

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

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

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

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

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.