Add math library - Githubissues

impermeable / coq-waterproof

The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.

https://impermeable.github.io/

GNU Lesser General Public License v3.0

30 stars 9 forks source link

Add math library #1

Closed jim-portegies closed 3 years ago

jim-portegies commented 3 years ago

Add math theory and adapt tactics:

Allow for terms that get coerced to types in the Take tactic
Enforce explicitly mentioning cases in case analysis