constants and parameters

Stream: condensed mathematics

[Johan Commelin]

For the first time in my life, I've used parameters. I think the constants file is now a lot cleaner:
https://github.com/leanprover-community/lean-liquid/commit/507a893a256620eac0feb2d36bf6749b6e59888e#diff-68815f57a2ad4caaf26391b1acb0cc82111d43b1acf122bb7d632ec0eb07f7a5

[Johan Commelin]

Roughly, it means that we don't have to pass around BD κ' r r' to every constant mentioned in the file.

[Johan Commelin]

I also noticed that when in tactic mode, you write have : blabla < N m it doesn't pass BD κ' r r' to N, so there the arguments become explicit anyways.

[Johan Commelin]

Not sure if that can be considered a bug. It would be nice if it works.

[Patrick Massot]

I remember telling you we should try that, but back then I was convinced by Mario that parameters were to buggy to help