Fix for problems with strong induction for defining index sequence.

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

29 stars 9 forks source link

Fix for problems with strong induction for defining index sequence. #38

Closed jellooo038 closed 9 months ago

jellooo038 commented 10 months ago

able to use property 'P(n(k)) = blue'
able to use notation 'n(k)' later on in proof
suggest 'n_0' instead of 'n0' to be more in line with suggested 'n_kplus1'