Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Irrelevance

Contents

Propositions
Fibrant types

Description

Proof-irrelevant propositions.

Synopsis

isPropM :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool
allPropTel :: (PureTCM m, MonadBlock m) => Telescope -> m Bool
isFibrant :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool
isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)
isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool)

Propositions

isPropM :: (LensSort a, PrettyTCM a, PureTCM m, MonadBlock m) => a -> m Bool Source #

Is a type a proposition? (Needs reduction.)

allPropTel :: (PureTCM m, MonadBlock m) => Telescope -> m Bool Source #

Fibrant types

isFibrant :: (LensSort a, PureTCM m, MonadBlock m) => a -> m Bool Source #

Is a type fibrant (i.e. Type, Prop)?

isFibrant' :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool) Source #

isCoFibrantSort :: (LensSort a, PureTCM m) => a -> m (Either Blocker Bool) Source #

Cofibrant types are those that could be the domain of a fibrant pi type. (Notion by C. Sattler).