Bugs and Tests

Possible bugs: It is not clear what the type should be of a FORALL. It is set so that it is either Type or Prop depending on what it contains.
Type Bug


Simplifies wrong:

Tests

This takes a term A and a term B and finds a function f such that f(A)=B

Example:

Simplifies wrongly:

Float should work here?
Should be `function`
// Float value not working [FIXED?]:

Broken

This breaks when you click SIMP. This stems from the times(x,x) line which breaks when it has two x's [WORKING?]. TOPOLOGY DEFINE RATIONAL POINTS ON CIRCLE: import Mathlib variable (CIRCLE: (forall (a:Rat), forall (b:Rat), (a^2+b^2=(1:Rat))->Type )) def a:= CIRCLE ((3:Rat)/5) ((4:Rat)/5) (by rfl) #print a #check a $$\sqrt{5}$$