Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[minor] incorrectly printed terms with type mismatch #4670

Closed
3 tasks done
fpvandoorn opened this issue Jul 6, 2024 · 0 comments · Fixed by #4982
Closed
3 tasks done

[minor] incorrectly printed terms with type mismatch #4670

fpvandoorn opened this issue Jul 6, 2024 · 0 comments · Fixed by #4982
Labels
bug Something isn't working P-low We are not planning to work on this issue

Comments

@fpvandoorn
Copy link
Contributor

Prerequisites

Please put an X between the brackets as you perform the following steps:

Description

The fact that Foo.out true is printed as true.out is confusing, since that looks like Bool.out true.

structure Foo : Type where
  out : Nat

/-
application type mismatch
  true.out
argument
  true
has type
  Bool : Type
but is expected to have type
  Foo : Type
-/
#check @Foo.out true

Expected behavior: true.out prints as Foo.out true

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

@fpvandoorn fpvandoorn added the bug Something isn't working label Jul 6, 2024
@fpvandoorn fpvandoorn changed the title [minor] incorrectly print terms with type mismatch [minor] incorrectly printed terms with type mismatch Jul 6, 2024
@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Aug 2, 2024
kmill added a commit to kmill/lean4 that referenced this issue Aug 11, 2024
For structure projections, the pretty printer assumed that the expression was type correct. Now it checks that the object being projected is of the correct type. Such terms appear in type mismatch errors.

Also, fixes and improves `#print` for structures. The types of projections now use MessageData (so are now hoverable), and the type of `self` is now the correct type.

Closes leanprover#4670
github-merge-queue bot pushed a commit that referenced this issue Aug 12, 2024
For structure projections, the pretty printer assumed that the
expression was type correct. Now it checks that the object being
projected is of the correct type. Such terms appear in type mismatch
errors.

Also, fixes and improves `#print` for structures. The types of
projections now use MessageData (so are now hoverable), and the type of
`self` is now the correct type.

Closes #4670
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-low We are not planning to work on this issue
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants