Unknown Identifier transR

Stream: new members

[Greg Leo]

`section

parameters {A : Type} {R : A → A → Prop}
parameter (reflR : reflexive R)
parameter (transR : transitive R)
def S (a b : A) : Prop := R a b ∧ R b a

example: transitive S :=
begin
assume a b c,
intro sab,
intro sbc,
have rab : R a b, from sab.left,
have rbc : R b c, from sbc.left,
have rba : R b a, from sab.right,
have rcb : R c b, from sbc.right,
split,
have rac : R a c, from transR ⟨rab⟩ ⟨rbc⟩,

end

end
`

I’m trying to prove an exercise from the lean manual. On this last line I get “unknown identifier transR` Is this because I need to import something that has the “transitive” definition?

[Ruben Van de Velde]

It might equally well have something to do with the use of parameter - mathlib tends to avoid it.

[Reid Barton]

It's because Lean doesn't know to include parameters (or variables) that are used only in the bodies of tactic blocks, for technical reasons.

[Reid Barton]

You can write include transR before example : transitive S :=.

[Greg Leo]

Ohhh! Worked. My first proof.

[Greg Leo]

In VS code, sometimes my ability to peek at definitions just goes away. Is this a known bug?

[Greg Leo]

A moment ago I could f12 to get definitions for highlighted terms. Now I can’t…

[Greg Leo]

But restarting vscode restores it.