1 include "basics/logic.ma".
3 \ 5img class="anchor" src="icons/tick.png" id="R"
\ 6axiom R : Type[0].
4 \ 5img class="anchor" src="icons/tick.png" id="add"
\ 6axiom add :
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6 →
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6 →
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6.
5 \ 5img class="anchor" src="icons/tick.png" id="times"
\ 6axiom times :
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6 →
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6 →
\ 5a href="cic:/matita/cicm2012/reals/R.dec"
\ 6R
\ 5/a
\ 6.
projects / helm.git / blob