paulch42
paulch42
# Dependent Type Theory ## Function Abstraction and Evaluation There is a statement "...has nothing to do with the constant ``b`` declared earlier." but there is no such declaration of...
In level 4 of Advanced Multiplication World there is a proof of: ``` theorem mul_left_cancel (a b c : MyNat) (ha : a ≠ 0) : a * b =...
Overture employs the ASCII syntax for model editing and output to TeX/PDF. If would be useful if the Latex menu item provided the option to generate TeX/PDF in the mathematical...
Some issues concerning the generation of LaTeX output from a model: 1 - sometimes keywords are not bolded correctly. 2 - Spurious blank lines are inserted. Attached are a simple...
### Description If a reference is made to a function or value from a different module using the fully qualified name but the module is not imported, an error is...
Overture has a feature that generates a LaTeX/PDF copy of a project. The output is fine as far as it goes, but it is static and while good for reading...
I use NetBeans for Java development and there are certain features I use repeatedly that are very convenient. They could be considered for inclusion in Overture (some are probably in...
In Overture all keywords have the same colour. In VSC two different colours are used. This approach has its benefits, but the two colours can lead to anomalies. For example,...