Safe Haskell	None
Language	Haskell2010

Language.PTS.Value

Contents

Values
Combinators
Application
Errors
Pairs
Equality
Prop types
Booleans
Natural numbers
Quarks
Pretty-printing

Synopsis

type Value s = ValueIntro Err s Sym
data ValueIntro err s a
- = ValueLam IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)
- | ValueCoerce (ValueElim err s a)
- | ValueSort s
- | ValuePi IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)
- | ValueErr err
- | ValueSigma IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)
- | ValuePair (ValueIntro err s a) (ValueIntro err s a)
- | ValueEquality (ValueIntro err s a) (ValueIntro err s a) (ValueIntro err s a)
- | ValueRefl
- | ValueUnit
- | ValueI
- | ValueEmpty
- | ValueBool
- | ValueTrue
- | ValueFalse
- | ValueNat
- | ValueNatZ
- | ValueNatS (ValueIntro err s a)
- | ValueHadron (Set Sym)
- | ValueQuark Sym
data ValueElim err s a
- = ValueApp (ValueElim err s a) (ValueIntro err s a)
- | ValueVar a
- | ValueMatch (ValueElim err s a) IrrSym IrrSym (Scope IrrSym2 (ValueIntro err s) a)
- | ValueJ (V3 IrrSym) (ValueIntro err s a) (Scope IrrSym3 (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)
- | ValueAbsurd (ValueIntro err s a) (ValueElim err s a)
- | ValueBoolElim IrrSym (Scope IrrSym (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)
- | ValueAnd (ValueElim err s a) (ValueElim err s a)
- | ValueNatElim IrrSym (Scope IrrSym (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)
- | ValuePlus (ValueElim err s a) (ValueElim err s a)
- | ValueTimes (ValueElim err s a) (ValueElim err s a)
- | ValueQuarkElim IrrSym (Scope IrrSym (ValueIntro err s) a) (Map Sym (ValueIntro err s a)) (ValueElim err s a)
pureValueIntro :: a -> ValueIntro err s a
pureValueElim :: a -> ValueElim err s a
mapValueIntroError :: (err -> err') -> ValueIntro err s a -> ValueIntro err' s a
valueApp :: (PrettyPrec err, AsErr err, Specification s) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
errorlessValueIntro :: MonadErr m => ValueIntro Err s a -> m (ValueIntro err' s a)
errorlessValueIntro' :: MonadErr m => ValueIntro Err s a -> m (ValueIntro Void s a)
errorlessValueElim :: MonadErr m => ValueElim Err s a -> m (ValueElim err' s a)
errorlessValueElim' :: MonadErr m => ValueElim Err s a -> m (ValueElim Void s a)
valueMatch :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> IrrSym -> IrrSym -> Scope IrrSym2 (ValueIntro err s) a -> ValueIntro err s a
valueJ :: (Specification s, AsErr err, PrettyPrec err) => V3 IrrSym -> ValueIntro err s a -> Scope IrrSym3 (ValueIntro err s) a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueAbsurd :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueBoolElim :: (Specification s, AsErr err, PrettyPrec err) => IrrSym -> Scope IrrSym (ValueIntro err s) a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueAnd :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueNatElim :: (Specification s, AsErr err, PrettyPrec err) => IrrSym -> Scope IrrSym (ValueIntro err s) a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valuePlus :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueTimes :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a
valueQuarkElim :: (Specification s, AsErr err, PrettyPrec err) => IrrSym -> Scope IrrSym (ValueIntro err s) a -> Map Sym (ValueIntro err s a) -> ValueIntro err s a -> ValueIntro err s a
pppIntro :: forall err s. (Specification s, PrettyPrec err) => Prec -> ValueIntro err s Doc -> PrettyM Doc
pppElim :: (Specification s, PrettyPrec err) => Prec -> ValueElim err s Doc -> PrettyM Doc

Values

type Value s = ValueIntro Err s Sym Source #

Value is in the normal form.

data ValueIntro err s a Source #

ValueIntro has a normal deduction, $A\!\uparrow$.

We assume that all operations are well-typed.

Constructors

ValueLam IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)	Implication introduction, lambda abstraction. \[ \frac {\color{darkblue}{\Gamma^\downarrow, x : \mathord{\tau\!\downarrow}} \vdash \color{darkgreen}b : \color{darkred}{\mathord{\tau'\!\uparrow}}} {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}{\lambda (a : \tau) \to b} : \color{darkred}{\mathord{\tau \to \tau'\!\uparrow}}} \]
ValueCoerce (ValueElim err s a)	Coercion. \[ \frac {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}x : \color{darkred}{\mathord{\tau\!\downarrow}}} {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}x : \color{darkred}{\mathord{\tau\!\uparrow}}} \]
ValueSort s	Sort introduction, axiom. \[ \frac {s_1 : s_2 \in \mathcal{A}} {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}{s_1} : \color{darkred}{s_2\!\uparrow}} \]
ValuePi IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)	Function type introduction. \[ \frac {(s_1, s_2, s_3 \in \mathcal{S}) \cdots} {\color{darkblue}{\Gamma^\downarrow} \vdash \cdots} \]
ValueErr err	Falsehood introduction, errors in evaluation, bottoms. \[ \frac {\color{darkblue}{\Gamma^\downarrow} \vdash - : \color{darkred}{\bot\!\downarrow}} {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}x : \color{darkred}{\tau\!\uparrow}} \]
ValueSigma IrrSym (ValueIntro err s a) (Scope IrrSym (ValueIntro err s) a)	Dependent pair (sum)
ValuePair (ValueIntro err s a) (ValueIntro err s a)	(Dependent) pair constructor
ValueEquality (ValueIntro err s a) (ValueIntro err s a) (ValueIntro err s a)	Equality
ValueRefl	Equality witness
ValueUnit
ValueI
ValueEmpty
ValueBool	Booleans.
ValueTrue	True.
ValueFalse	False.
ValueNat	Nat type
ValueNatZ	Nat zero
ValueNatS (ValueIntro err s a)	Nat successor
ValueHadron (Set Sym)	Hadron (collection of quarks) type.
ValueQuark Sym	Quark.

Instances

ValueConv ValueIntro Source #
Instance details Defined in Language.PTS.Smart Methods toValueIntro :: ValueIntro err s a -> ValueIntro err s a Source #
Quote ValueIntro TermChk Source #
Instance details Defined in Language.PTS.Quote Methods quote_ :: Specification s => ValueIntro Void s a -> TermChk s a Source #
CanSort (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods sort_ :: s -> ValueIntro err s a Source #
CanPi (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods pi_ :: Sym -> ValueIntro err s Sym -> ValueIntro err s Sym -> ValueIntro err s Sym Source # (~>) :: Specification s => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source # sigma_ :: Sym -> ValueIntro err s Sym -> ValueIntro err s Sym -> ValueIntro err s Sym Source #
Convert (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods convert :: ValueIntro err s a -> ValueIntro err s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueIntro err s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueElim err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueElim err s a Source #
(PrettyPrec err, AsErr err, Specification s) => Monad (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods (>>=) :: ValueIntro err s a -> (a -> ValueIntro err s b) -> ValueIntro err s b Source # (>>) :: ValueIntro err s a -> ValueIntro err s b -> ValueIntro err s b Source # return :: a -> ValueIntro err s a Source # fail :: String -> ValueIntro err s a Source #
Functor (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods fmap :: (a -> b) -> ValueIntro err s a -> ValueIntro err s b Source # (<$) :: a -> ValueIntro err s b -> ValueIntro err s a Source #
(PrettyPrec err, AsErr err, Specification s) => Applicative (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods pure :: a -> ValueIntro err s a Source # (<>) :: ValueIntro err s (a -> b) -> ValueIntro err s a -> ValueIntro err s b Source # liftA2 :: (a -> b -> c) -> ValueIntro err s a -> ValueIntro err s b -> ValueIntro err s c Source # (>) :: ValueIntro err s a -> ValueIntro err s b -> ValueIntro err s b Source # (<*) :: ValueIntro err s a -> ValueIntro err s b -> ValueIntro err s a Source #
Foldable (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods fold :: Monoid m => ValueIntro err s m -> m Source # foldMap :: Monoid m => (a -> m) -> ValueIntro err s a -> m Source # foldr :: (a -> b -> b) -> b -> ValueIntro err s a -> b Source # foldr' :: (a -> b -> b) -> b -> ValueIntro err s a -> b Source # foldl :: (b -> a -> b) -> b -> ValueIntro err s a -> b Source # foldl' :: (b -> a -> b) -> b -> ValueIntro err s a -> b Source # foldr1 :: (a -> a -> a) -> ValueIntro err s a -> a Source # foldl1 :: (a -> a -> a) -> ValueIntro err s a -> a Source # toList :: ValueIntro err s a -> [a] Source # null :: ValueIntro err s a -> Bool Source # length :: ValueIntro err s a -> Int Source # elem :: Eq a => a -> ValueIntro err s a -> Bool Source # maximum :: Ord a => ValueIntro err s a -> a Source # minimum :: Ord a => ValueIntro err s a -> a Source # sum :: Num a => ValueIntro err s a -> a Source # product :: Num a => ValueIntro err s a -> a Source #
Traversable (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods traverse :: Applicative f => (a -> f b) -> ValueIntro err s a -> f (ValueIntro err s b) Source # sequenceA :: Applicative f => ValueIntro err s (f a) -> f (ValueIntro err s a) Source # mapM :: Monad m => (a -> m b) -> ValueIntro err s a -> m (ValueIntro err s b) Source # sequence :: Monad m => ValueIntro err s (m a) -> m (ValueIntro err s a) Source #
Eq s => Eq1 (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods liftEq :: (a -> b -> Bool) -> ValueIntro err s a -> ValueIntro err s b -> Bool Source #
(Show s, Show err) => Show1 (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ValueIntro err s a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ValueIntro err s a] -> ShowS Source #
(Specification s, PrettyPrec err) => PrettyPrec1 (ValueIntro err s) Source #
Instance details Defined in Language.PTS.Value Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> ValueIntro err s a -> PrettyM Doc Source #
(PrettyPrec err, AsErr err, Specification s) => Module (ValueIntro err s) (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods (>>==) :: ValueIntro err s a -> (a -> ValueElim err s b) -> ValueIntro err s b #
(Eq a, Eq s) => Eq (ValueIntro err s a) Source #
Instance details Defined in Language.PTS.Value Methods (==) :: ValueIntro err s a -> ValueIntro err s a -> Bool Source # (/=) :: ValueIntro err s a -> ValueIntro err s a -> Bool Source #
(Show a, Show err, Show s) => Show (ValueIntro err s a) Source #
Instance details Defined in Language.PTS.Value Methods showsPrec :: Int -> ValueIntro err s a -> ShowS Source # show :: ValueIntro err s a -> String Source # showList :: [ValueIntro err s a] -> ShowS Source #
IsString a => IsString (ValueIntro err s a) Source #
Instance details Defined in Language.PTS.Value Methods fromString :: String -> ValueIntro err s a Source #
(Specification s, PrettyPrec err, PrettyPrec a) => PrettyPrec (ValueIntro err s a) Source #
Instance details Defined in Language.PTS.Value Methods ppp :: Prec -> ValueIntro err s a -> PrettyM Doc Source #

data ValueElim err s a Source #

ValueElim is extracted from a hypothesis, $A\!\downarrow$.

Constructors

ValueApp (ValueElim err s a) (ValueIntro err s a)	Implication elimination, application. \[ \frac {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}f : \color{darkred}{\tau \to \tau'\!\downarrow} \qquad \color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}x : \color{darkred}{\tau\!\uparrow}} {\color{darkblue}{\Gamma^\downarrow} \vdash \color{darkgreen}{f\,x} : \color{darkred}{\tau'\!\downarrow}} \]
ValueVar a	Hypothesis, variable. \[ \frac{} {\color{darkblue}{\Gamma^\downarrow, x : \mathord{\tau\!\downarrow}} \vdash \color{darkgreen}x : \color{darkred}{\tau\!\downarrow}} \]
ValueMatch (ValueElim err s a) IrrSym IrrSym (Scope IrrSym2 (ValueIntro err s) a)	Dependent pattern match on a pair. match p (x y -> b) ~ (x y -> b) (fst p) (snd p)
ValueJ (V3 IrrSym) (ValueIntro err s a) (Scope IrrSym3 (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)	Equality elmination
ValueAbsurd (ValueIntro err s a) (ValueElim err s a)
ValueBoolElim IrrSym (Scope IrrSym (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)	Boolean elimination
ValueAnd (ValueElim err s a) (ValueElim err s a)	Boolean conjunction
ValueNatElim IrrSym (Scope IrrSym (ValueIntro err s) a) (ValueIntro err s a) (ValueIntro err s a) (ValueElim err s a)	Natural number elimination
ValuePlus (ValueElim err s a) (ValueElim err s a)	Natural number addition
ValueTimes (ValueElim err s a) (ValueElim err s a)	Natural number multiplication
ValueQuarkElim IrrSym (Scope IrrSym (ValueIntro err s) a) (Map Sym (ValueIntro err s a)) (ValueElim err s a)	Hadron elimination.

Instances

ValueConv ValueElim Source #
Instance details Defined in Language.PTS.Smart Methods toValueIntro :: ValueElim err s a -> ValueIntro err s a Source #
Quote ValueElim TermInf Source #
Instance details Defined in Language.PTS.Quote Methods quote_ :: Specification s => ValueElim Void s a -> TermInf s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueIntro err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueIntro err s a Source #
CanApp (ValueElim err) (ValueIntro err) (ValueElim err) Source #
Instance details Defined in Language.PTS.Smart Methods (@@) :: ValueElim err s a -> ValueIntro err s a -> ValueElim err s a Source #
(PrettyPrec err, AsErr err, Specification s) => Monad (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods (>>=) :: ValueElim err s a -> (a -> ValueElim err s b) -> ValueElim err s b Source # (>>) :: ValueElim err s a -> ValueElim err s b -> ValueElim err s b Source # return :: a -> ValueElim err s a Source # fail :: String -> ValueElim err s a Source #
Functor (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods fmap :: (a -> b) -> ValueElim err s a -> ValueElim err s b Source # (<$) :: a -> ValueElim err s b -> ValueElim err s a Source #
(PrettyPrec err, AsErr err, Specification s) => Applicative (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods pure :: a -> ValueElim err s a Source # (<>) :: ValueElim err s (a -> b) -> ValueElim err s a -> ValueElim err s b Source # liftA2 :: (a -> b -> c) -> ValueElim err s a -> ValueElim err s b -> ValueElim err s c Source # (>) :: ValueElim err s a -> ValueElim err s b -> ValueElim err s b Source # (<*) :: ValueElim err s a -> ValueElim err s b -> ValueElim err s a Source #
Foldable (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods fold :: Monoid m => ValueElim err s m -> m Source # foldMap :: Monoid m => (a -> m) -> ValueElim err s a -> m Source # foldr :: (a -> b -> b) -> b -> ValueElim err s a -> b Source # foldr' :: (a -> b -> b) -> b -> ValueElim err s a -> b Source # foldl :: (b -> a -> b) -> b -> ValueElim err s a -> b Source # foldl' :: (b -> a -> b) -> b -> ValueElim err s a -> b Source # foldr1 :: (a -> a -> a) -> ValueElim err s a -> a Source # foldl1 :: (a -> a -> a) -> ValueElim err s a -> a Source # toList :: ValueElim err s a -> [a] Source # null :: ValueElim err s a -> Bool Source # length :: ValueElim err s a -> Int Source # elem :: Eq a => a -> ValueElim err s a -> Bool Source # maximum :: Ord a => ValueElim err s a -> a Source # minimum :: Ord a => ValueElim err s a -> a Source # sum :: Num a => ValueElim err s a -> a Source # product :: Num a => ValueElim err s a -> a Source #
Traversable (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods traverse :: Applicative f => (a -> f b) -> ValueElim err s a -> f (ValueElim err s b) Source # sequenceA :: Applicative f => ValueElim err s (f a) -> f (ValueElim err s a) Source # mapM :: Monad m => (a -> m b) -> ValueElim err s a -> m (ValueElim err s b) Source # sequence :: Monad m => ValueElim err s (m a) -> m (ValueElim err s a) Source #
Eq s => Eq1 (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods liftEq :: (a -> b -> Bool) -> ValueElim err s a -> ValueElim err s b -> Bool Source #
(Show s, Show err) => Show1 (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ValueElim err s a -> ShowS Source # liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ValueElim err s a] -> ShowS Source #
(Specification s, PrettyPrec err) => PrettyPrec1 (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods liftPpp :: (Prec -> a -> PrettyM Doc) -> Prec -> ValueElim err s a -> PrettyM Doc Source #
(PrettyPrec err, AsErr err, Specification s) => Module (ValueIntro err s) (ValueElim err s) Source #
Instance details Defined in Language.PTS.Value Methods (>>==) :: ValueIntro err s a -> (a -> ValueElim err s b) -> ValueIntro err s b #
(Eq a, Eq s) => Eq (ValueElim err s a) Source #
Instance details Defined in Language.PTS.Value Methods (==) :: ValueElim err s a -> ValueElim err s a -> Bool Source # (/=) :: ValueElim err s a -> ValueElim err s a -> Bool Source #
(Show a, Show err, Show s) => Show (ValueElim err s a) Source #
Instance details Defined in Language.PTS.Value Methods showsPrec :: Int -> ValueElim err s a -> ShowS Source # show :: ValueElim err s a -> String Source # showList :: [ValueElim err s a] -> ShowS Source #
IsString a => IsString (ValueElim err s a) Source #
Instance details Defined in Language.PTS.Value Methods fromString :: String -> ValueElim err s a Source #
(Specification s, PrettyPrec err, PrettyPrec a) => PrettyPrec (ValueElim err s a) Source #
Instance details Defined in Language.PTS.Value Methods ppp :: Prec -> ValueElim err s a -> PrettyM Doc Source #

Combinators

pureValueIntro :: a -> ValueIntro err s a Source #

pureValueElim :: a -> ValueElim err s a Source #

mapValueIntroError :: (err -> err') -> ValueIntro err s a -> ValueIntro err' s a Source #

Application

valueApp Source #

Arguments

:: (PrettyPrec err, AsErr err, Specification s)
=> ValueIntro err s a	f : a -> b
-> ValueIntro err s a	x : a
-> ValueIntro err s a	_ : b

Apply to values.

Note that @@ from Language.PTSmart module is different

Errors

errorlessValueIntro :: MonadErr m => ValueIntro Err s a -> m (ValueIntro err' s a) Source #

errorlessValueIntro' :: MonadErr m => ValueIntro Err s a -> m (ValueIntro Void s a) Source #

errorlessValueElim :: MonadErr m => ValueElim Err s a -> m (ValueElim err' s a) Source #

errorlessValueElim' :: MonadErr m => ValueElim Err s a -> m (ValueElim Void s a) Source #

Pairs

valueMatch :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> IrrSym -> IrrSym -> Scope IrrSym2 (ValueIntro err s) a -> ValueIntro err s a Source #

Equality

valueJ :: (Specification s, AsErr err, PrettyPrec err) => V3 IrrSym -> ValueIntro err s a -> Scope IrrSym3 (ValueIntro err s) a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source #

Prop types

valueAbsurd :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source #

Booleans

valueBoolElim Source #

Arguments

:: (Specification s, AsErr err, PrettyPrec err)
=> IrrSym	x
-> Scope IrrSym (ValueIntro err s) a	P : s
-> ValueIntro err s a	t : P true
-> ValueIntro err s a	f : P false
-> ValueIntro err s a	b : Bool
-> ValueIntro err s a	P b

valueAnd :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source #

Natural numbers

valueNatElim Source #

Arguments

:: (Specification s, AsErr err, PrettyPrec err)
=> IrrSym	x
-> Scope IrrSym (ValueIntro err s) a	P : s
-> ValueIntro err s a	z : P 0
-> ValueIntro err s a	f : (forall l. P l -> P (succ l)
-> ValueIntro err s a	n : Nat
-> ValueIntro err s a	P n

valuePlus :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source #

valueTimes :: (Specification s, AsErr err, PrettyPrec err) => ValueIntro err s a -> ValueIntro err s a -> ValueIntro err s a Source #

Quarks

valueQuarkElim :: (Specification s, AsErr err, PrettyPrec err) => IrrSym -> Scope IrrSym (ValueIntro err s) a -> Map Sym (ValueIntro err s a) -> ValueIntro err s a -> ValueIntro err s a Source #

Pretty-printing

pppIntro :: forall err s. (Specification s, PrettyPrec err) => Prec -> ValueIntro err s Doc -> PrettyM Doc Source #

pppElim :: (Specification s, PrettyPrec err) => Prec -> ValueElim err s Doc -> PrettyM Doc Source #