Skip to main content
PRL Project



next up previous
Next: References Up: Formalizing Constructive Real Analysis Previous: Tactics

Tactic Code

The tactics described above, together with some special-purpose lemmas to which they refer.

For readability, different notations have been used in the following theorems. a. is the rational number a/1.

Again we use some more visible notation. a is the real number i.a.