Angle brackets precidence

[rspencer01]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

ASCII angle brackets of the form (| ... |) and pretty angle brackets ⟨ ... ⟩ appear to take different precedence, and so behave differently.

Steps to Reproduce

1. Attempt to run lean against the following file (which is the example I have on hand and not necessarily a MWE)

variables (A : Type) (p q : A -> Prop)

variable a : A

example : (exists x , p x \/ q x) -> (exists x , p x ) \/ (exists x , q x) :=
    assume (| a, (pqa : p a \/ q a) |),
    or.elim pqa
      (
        assume hpa : p a, or.inl ⟨a, hpa⟩
      )
      (
        assume hqa : q a, or.inr (|a, hqa|)
        --assume hqa : q a, or.inr ( (|a, hqa|) )
        --assume hqa : q a, or.inr ⟨a, hqa⟩
      )

Expected behavior: No output

Actual behavior: Error output

/tmp/t.lean:12:33: error: invalid expression, `)` expected
/tmp/t.lean:12:33: error: command expected
/tmp/t.lean:7:4: error: type mismatch at application
  or.elim pqa (λ (hpa : p a), or.inl (Exists.intro a hpa)) (λ (hqa : q a), or.inr)
term
  λ (hqa : q a), or.inr
has type
  Π (hqa : q a), ?m_1[hqa] → ?m_2[hqa] ∨ ?m_1[hqa]
but is expected to have type
  q a → ((∃ (x : A), p x) ∨ ∃ (x : A), q x)

This goes away if either of the two commented out lines is substituted back in.

Reproduces how often: Always

Versions

Lean (version 3.4.2, commit cbd2b6686ddb, Release)

Operating system

Distributor ID:	Ubuntu
Description:	Ubuntu 16.04.5 LTS
Release:	16.04
Codename:	xenial