[Agda] Re: proofs with "with"

Stefan Monnier monnier at iro.umontreal.ca
Mon Dec 15 21:02:51 CET 2014


> That is, it usually makes your life easier if you don't use "with"
> in definitions that you later will want to prove something about.

Reminds me of the the Coq situation where it's recommended not to use
tactics for definitions.


        Stefan



More information about the Agda mailing list