Solving (or not) linear equations

siddhartha-gadgil / LTS2019

Web page, code for "Logic, Types Spaces 2019" at IISc

http://math.iisc.ac.in/~gadgil/LTS2019/

MIT License

9 stars 13 forks source link

Open siddhartha-gadgil opened 5 years ago

siddhartha-gadgil commented 5 years ago

Given linear equations (one to start with, several eventually) return a type that is either
- a solution with a proof that it is a solution (one may need to pull in an implementation of rationals, say from https://github.com/mcgordonite/idris-binary-rationals)
- a proof that there is no solution
Further one can either show uniqueness or lack of uniqueness.

siddhartha-gadgil commented 5 years ago

Rather than using an implementation of rationals, one should define fields and work over a field.
Constructing a field of rationals is a separate issue.