constant, variable, parameter

Stream: lean4

[Martin Dvořák]

Will the section-wide declarations constant and variable and parameter still work in lean4?

[Horațiu Cheval]

parameter for one is no longer a thing. See for instance this thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/parameter

[Henrik Böving]

Furthermore we renamed constant to opaque. We still have variable but no variables anymore, variable now covers both single and multiple variable declarations.

[Horațiu Cheval]

And opaque doesn't seem to be per section, right?

  section
    opaque C : Nat
  end
  #check C
  -- C : ℕ

[Henrik Böving]

No, it also shouldn't be, I'd be surprised if it was this way in Lean 3. opaque/constant is a real declaration that should be limited to namespaces not sections.

[Martin Dvořák]

How was parameter broken in lean3?

[Mac]

Henrik Böving said:

Furthermore we renamed constant to opaque.

Despite its previous name, opaque has nothing to with Lean 3's constant.

[Simon Hudon]

@Martin Dvořák when you’re writing out a term, parameter does what you’d expect: it is treated more like a global constant than an argument to your definitions. So far so good. In a tactic however, it’s as if you had declared it as a variable. You can’t omit it anymore in your function applications