angle brackets

Stream: new members

[Jeremy Teitelbaum]

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]

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

[Mario Carneiro]

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]

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]

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