See interactive version.
In this work we will define a superset of integers (the complete integers), which contains the dual of integers along parity (e.g. the odd zero, the even one, ...). Then we will see how they form a ring and how they can be used as exponents for real numbers powers, in order to write functions which have a discontinuity in zero (the function itself or one of its derivates), as for example the absolute value and the sign function.
- Clone the repo https://gitlab.com/DPDmancul/complete-integers-agda.git
- Optionally run
nix-shellto get all the required dependencies into the environment - Just run
maketo build all;make html,make pdformake epubto build only one format.
(c) 2022 Davide Peressoni
This work is licensed under both the Apache 2.0 License and the Creative Commons Attribution-ShareAlike 4.0 International License.
Attribution -- You must give appropriate credit, provide a link to the license, and indicate if changes were made. You may do so in any reasonable manner, but not in any way that suggests the licensor endorses you or your use.
ShareAlike -- If you remix, transform, or build upon the material, you must distribute your contributions under the same license as the original.
Created with Agda and R bookdown.
The source files can be found at https://gitlab.com/DPDmancul/complete-integers-agda.