Zulip Chat Archive
Stream: general
Topic: level.imax
Sean Leather (Jul 16 2018 at 06:55):
What is level.imax?
Sean Leather (Jul 16 2018 at 06:59):
Never mind, found it: “where imax i j is the maximum of i and j if j is not 0, and 0 otherwise.”
https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html?highlight=imax#the-universal-quantifier
Last updated: May 02 2025 at 03:31 UTC