diff options
| author | Vincent Semeria | 2019-06-27 23:35:03 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-07-16 18:45:34 +0200 |
| commit | eebc676ce4978b7e408c427889bae356d8b0efdc (patch) | |
| tree | 2bc6228c80817026d4e2108e871867fc50a86fa2 /doc/plugin_tutorial/tuto2/src/custom.ml | |
| parent | 3bd2722fb53552f45a25e6bc0a03a9ab0517485f (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/tuto2/src/custom.ml')
0 files changed, 0 insertions, 0 deletions