aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1
diff options
context:
space:
mode:
authorVincent Semeria2019-06-27 23:35:03 +0200
committerVincent Semeria2019-07-16 18:45:34 +0200
commiteebc676ce4978b7e408c427889bae356d8b0efdc (patch)
tree2bc6228c80817026d4e2108e871867fc50a86fa2 /doc/plugin_tutorial/tuto1
parent3bd2722fb53552f45a25e6bc0a03a9ab0517485f (diff)
Define constructive real numbers as Cauchy sequences of rational numbers. Redefine classical real numbers as a quotient of those constructive real numbers.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions