Zulip Chat Archive

Stream: new members

Topic: Unknown Identifier transR


Greg Leo (Dec 14 2021 at 19:00):

`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 (Dec 14 2021 at 19:06):

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

Reid Barton (Dec 14 2021 at 19:14):

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 (Dec 14 2021 at 19:15):

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

Greg Leo (Dec 14 2021 at 19:23):

Ohhh! Worked. My first proof.

Greg Leo (Dec 14 2021 at 19:37):

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

Greg Leo (Dec 14 2021 at 19:37):

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

Greg Leo (Dec 14 2021 at 19:39):

But restarting vscode restores it.


Last updated: Dec 20 2023 at 11:08 UTC