Confused about parameters

Stream: new members

[Dan Piponi]

I'm working on a basic exercise:

parameters {A : Type} {R : A → A → Prop}
parameter (transR : transitive R)

local infix < := R

def R' (a b : A) : Prop := R a b ∨ a = b
local infix ≤ := R'

theorem transR' {a b c : A} (h1 : a ≤ b) (h2 : b ≤ c):
  a ≤ c :=
begin
  cases h1,
  cases h2,
  left,
  exact transR h1 h2,
end
end

I get unknown identifier 'transR'. But there it is at the top: parameter (transR : transitive R). I must be misunderstanding what parameter means. So what does parameter mean?

[Johan Commelin]

I think it's only included automatically in declarations that mention it in their type.

[Johan Commelin]

Does include transR before your theorem solve the issue?

[Dan Piponi]

That certainly allows my step in the proof to go through, thanks. (I guess I still need to think about what work parameter is doing here.)

[Johan Commelin]

@Dan Piponi For example, you could make {a b c : A} parameters (or variables) and then you wouldn't need to include them explicitly. Why? Because h1 and h2 mention them, so Lean knows to pull them in.

[Johan Commelin]

transR was only mentioned in the begin .. end block, but by the time Lean is digesting that, it is past the phase of deciding which variables/parameters to pull into the statement.

[Johan Commelin]

With include you instruct Lean to just pull it into every statement directly.