Next: Compatible fonctions Up: User's manual of the Previous: Defining functions by induction Contents

Basic definitions

$\begin{sort}[]~ \begin{center}set \end{center}\end{sort}$

$\begin{constant}[]~ \begin{center}% \afdmath{}\text{\rm D}\endafdmath{} : set $\... ...ow$\ prop \SaveVerb{Verb}訴跚marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{constant}[]~ \begin{center}% \afdmath{}\text{\rm R}\endafdmath{} : set $\... ...ow$\ prop \SaveVerb{Verb}買跚marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{axiom}[% \afdmath{}\text{\rm refl}.\text{\rm Q}\endafdmath{}]~ \afdmmath{... ...rm D}\ibreak{0.2em}{2.em} \text{\rm R}\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{axiom}[% \afdmath{}\text{\rm sym}.\text{\rm Q}\endafdmath{}]~ \afdmmath{}... ...rm D}\ibreak{0.2em}{2.em} \text{\rm R}\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{axiom}[% \afdmath{}\text{\rm trans}.\text{\rm Q}\endafdmath{}]~ \afdmmath... ...rm D}\ibreak{0.2em}{2.em} \text{\rm R}\endprettybox{}\endafdmmath{} \end{axiom}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm Q}\hspace{0.2em} \text... ...ath{} \SaveVerb{Verb}貴 X跚marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{definition}[]~ \begin{center}% \afdmath{}\text{\rm class}\hspace{0.2em} \... ...\SaveVerb{Verb}軼lass x y跚marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{proposition}[% \afdmath{}\text{\rm class}.\text{\rm Q}\endafdmath{}]~ \af... ...ext{\it x}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{proposition}$

class.Q added as introduction rule (abbrev: class , options: -c )

$\begin{proposition}[% \afdmath{}\text{\rm equal}.\text{\rm class}.\text{\rm Q}\e... ...rettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

equal.class.Q added as equation

$\begin{proposition}[% \afdmath{}\text{\rm class}.\text{\rm inj}.\text{\rm Q}\end... ...ext{\it y}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

$\begin{proposition}[% \afdmath{}\text{\rm class}.\text{\rm elim}\endafdmath{}]~ ... ...36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

class.elim added as elimination rule (abbrev: rec , options: -i )

$\begin{proposition}[% \afdmath{}\text{\rm equal}.\text{\rm Q}\endafdmath{}]~ \af... ...ext{\it y}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{proposition}$

equal.Q added as introduction rule (abbrev: equal , options: -i )

Christophe Raffalli 2005-03-02