You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
set_option quotPrecheck.allowSectionVars true
variable (O : Type) (rel : O → O → Prop)
infixl:50" ◃ " => rel
theoremfoo : ∀ x y : O, x ◃ y :=
by/- Goal is `∀ (x y : O), rel x y` -/ admit
More precisely :
set_option quotPrecheck.allowSectionVars true
variable (O : Type) (rel : O → O → Prop)
infixl:50" ◃ " => rel
@[appUnexpander rel]defunexpandRel : Lean.PrettyPrinter.Unexpander
| `(rel $x $y) => `($x ◃ $y)
| _ => throw ()
theoremfoo : ∀ x y : O, rel x y :=
by/- Goal is `∀ (x y : O), rel x y` -/ admit
Expected behavior: The goal should be ∀ (x y : O), x ◃ y (and the relation should also be correctly pretty printed by #print).
Actual behavior: It is ∀ (x y : O), rel x y (#print's result is wrong too).
set_option quotPrecheck.allowSectionVars true
variable (O : Type) (rel : O → O → Prop)
infixl:50" ◃ " => id rel
@[appUnexpander id]defunexpandAppRel : Lean.PrettyPrinter.Unexpander
| `(id rel $x $y) => `($x ◃ $y)
| _ => throw ()
theoremfoo : ∀ x y : O, x ◃ y :=
by/- Goal is now `∀ (x y : O), x ◃ y` ! -/ admit
This satisfies appUnexpander's requirement that app have a global name, but it would be best to be able to just refer to a local variable.
Possible extension
It might be interesting to have appUnexpander accept more complex right hand sides : in the current state, and up to my knowledge, it only accepts functions (syntactically, i.e. function applications don't count there, even if they type as function).
For instance, someone might write :
infixl:50" ◃ " => Group.mul G
which wouldn't be supported at the current state of appUnexpander's implementation
The text was updated successfully, but these errors were encountered:
Prerequisites
Description
Custom notations that refer to local variables aren't correctly delaborated.
This appears to be related to how
appUnexpander
s behave : up to my understanding,appUnexpander
s only accept function that have a global name.Also described here.
Related to #435 and #358
Steps to Reproduce
More precisely :
Expected behavior: The goal should be
∀ (x y : O), x ◃ y
(and the relation should also be correctly pretty printed by#print
).Actual behavior: It is
∀ (x y : O), rel x y
(#print
's result is wrong too).Versions
Lean (version 4.0.0-nightly-2021-05-13, commit 0eaa36b, Release)
Ubuntu 20.04.2 LTS
Additional Information
There is a workaround :
This satisfies
appUnexpander
's requirement thatapp
have a global name, but it would be best to be able to just refer to a local variable.Possible extension
It might be interesting to have
appUnexpander
accept more complex right hand sides : in the current state, and up to my knowledge, it only accepts functions (syntactically, i.e. function applications don't count there, even if they type as function).For instance, someone might write :
which wouldn't be supported at the current state of
appUnexpander
's implementationThe text was updated successfully, but these errors were encountered: