Zulip Chat Archive

Stream: condensed mathematics

Topic: constants and parameters


Johan Commelin (Jun 25 2021 at 08:51):

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 (Jun 25 2021 at 08:52):

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

Johan Commelin (Jun 25 2021 at 08:53):

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 (Jun 25 2021 at 08:53):

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

Patrick Massot (Jun 25 2021 at 09:17):

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


Last updated: Dec 20 2023 at 11:08 UTC