Irene Lobo Valbuena
Irene Lobo Valbuena
In accordance to the actual definition of a module vs a vector space in mathematics (given the current `Ring` constraint on the associated type family `Scalar` of the class `VectorSpace`,...
Such as those converting to and from 'Double' in ['Field'](https://github.com/Airini/FEECa/blob/master/src/FEECa/Internal/Spaces.hs). So far, they are seen in: * (pretty) printing * testing, e.g. ['eqNum'](https://github.com/Airini/FEECa/blob/master/src/FEECa/Utility/Utility.hs) to account for margins of numerical error...
_Check out mail_, so as to carry on with the writing and polishing of FEECa. Merge changes in implementation and/or documentation into the main branch (when ready and tested).
Handle the proof search to have the concrete recursion induction scheme (or lack thereof) and induction variables that succeed be identified at the end.
Equality `=` is translated by Isabelle into Haskell as a new function definition `equal_T` (with `T` the type). HipSpec gets an additional function, obtaining corresponding properties. When brought back into...