Zulip Chat Archive

Stream: new members

Topic: anonymous angle brackets


Robert Watson (Mar 05 2022 at 16:40):

I've come across anonymous angle brackets and in the Tutorials (I'm using Lean 3). What actually are these in terms of types? Is this notation for a sigma type (in the Tutorials it looks more like a Cartesian product)? What actually is the full syntax for these angle brackets - when exactly does one use them? But in the example (below) normal parentheses are used for what I think must be a sigma type, so I'm finding this confusing...

I understand that there are differences between tactics as to how parentheses are used, and then presumably the same again outside tactics mode. So what handle do I need on this to make sense of the different uses?

example {x y : } : ( ε > 0, y  x + ε)   y  x :=
begin
  contrapose!,
  intro h,
  exact ⟨(y-x)/2, by linarith, by linarith⟩,
end

Last updated: Dec 20 2023 at 11:08 UTC