Zulip Chat Archive

Stream: new members

Topic: angle brackets


Jeremy Teitelbaum (Dec 08 2021 at 16:47):

Hi all, I am working through Kevin's course and I don't understand the meaning of the angle brackets -- what is their significance in a statement like:

rintros \< hA, hB\>

Kevin Buzzard (Dec 08 2021 at 16:48):

If you change rintros \< hA, hB\> to intro X then you'll be able to see the type of X.

Mario Carneiro (Dec 08 2021 at 16:48):

It's used to destructure a tuple-like type. In this case your goal is probably something like A /\ B -> C and that line will change it to hA : A, hB : B |- C

Kevin Buzzard (Dec 08 2021 at 16:49):

And what will be happening is that to make a term of type X you'll need to give two other terms. For example, as Mario says, if the type of X is A \and B then to give a term of this type is to give a proof of A and a proof of B, and you can get those terms with cases X with hA hB. rintro is just doing the intro and the cases all at once.

Kevin Buzzard (Dec 08 2021 at 16:51):

import tactic

example (A B C : Prop) : A  B  C :=
begin
  intro h,
  cases h with hA hB,
  /-
  A B C: Prop
  hA : A
  hB : B
  ⊢ C
  -/
  sorry
end

example (A B C : Prop) : A  B  C :=
begin
  rintro hA, hB⟩,
  /-
  A B C: Prop
  hA : A
  hB : B
  ⊢ C
  -/
  sorry
end

Last updated: Dec 20 2023 at 11:08 UTC