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
Description
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.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
ASCII angle brackets of the form (| ... |)
and pretty angle brackets ⟨ ... ⟩
appear to take different precedence, and so behave differently.
Steps to Reproduce
- 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
Labels
No labels