Skip to content
This repository was archived by the owner on Oct 14, 2023. It is now read-only.
This repository was archived by the owner on Oct 14, 2023. It is now read-only.

Angle brackets precidence #1992

Open
Open
@rspencer01

Description

@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.
    • 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

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions