search

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

Feat binders #71

Closed jim-portegies closed 1 month ago

jim-portegies commented 1 month ago

Check for binder names in Choose and Take tactics.

For instance

Goal exists n : nat, n + 1 = n + 1.
    Choose m := 1.
Abort.

generates a warning, as does

Goal forall n : nat, n = n.
Proof.
  Take m : nat.
Abort.
jim-portegies commented 1 month ago

Note that the following also generates a warning, and that m is renamed into n

Goal forall m n : nat, True.
Take n : nat.
Abort.