Skip to content

RFC: unexpanders take priority#526

Merged
Kha merged 1 commit intoleanprover:masterfrom
dselsam:unexpand_order
Jun 13, 2021
Merged

RFC: unexpanders take priority#526
Kha merged 1 commit intoleanprover:masterfrom
dselsam:unexpand_order

Conversation

@dselsam
Copy link
Contributor

@dselsam dselsam commented Jun 12, 2021

This PR addresses an issue raised by @dwrensha at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/controlling.20delaboration. Currently, unexpanders for structures are ignored since they are tried after the builtin structure unexpanders. Example:

structure Foo where
  x : Nat
  y : Nat

syntax term "" term : term

macro_rules
| `( $a ♬ $b ) => `(Foo.mk $a $b)

#check 12 -- { x := 1, y := 2 }

@[appUnexpander Foo] def unexpandFoo : Lean.PrettyPrinter.Unexpander
  | `({ x:= $a, y:= $b }) => `($a ♬ $b)
  | _ => throw ()

#check 34 -- { x := 3, y := 4 } 

At @Kha's suggestion, this PR avoids the need to cache calls within the delaborator at the cost of requiring exponential time on an obscure edge case in which a stack of unexpanders all fail. The issue is documented in the code in case there is interest in addressing it in the future.

@Kha Kha merged commit 51d26e1 into leanprover:master Jun 13, 2021
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this pull request Dec 2, 2022
TODO:
* Before merge
- [x] fix a bug in linarith in mathlib3 I just found ...
- [x] depends on: leanprover#519 
- [x] style lint
- [x] docs
- [X] move theory stubs to a separate PR, for easier tracking: leanprover#733 
- [x] failing to parse the `LinarithConfig` option

* Before or after merge?
- [ ] Implement the `removeNe` preprocessor.
- [ ] Add support for restricting to a single type. How to store a `Type` in `LinarithConfig`?

* After merge
- [ ] Teach `norm_num` to solve `example [LinearOrderedRing α] : (0 : α) < 37 := by norm_num`.
- [ ] Port `zify_proof` (plumbing for `zify`), and add the `natToInt` preprocessor.
  Mostly done now, but see leanprover#741 before all the tests will work.
- [ ] Port `cancel_denoms` tactic, and add the `cancelDenoms` preprocessor.
- [ ] Add the `nlinarith` preprocessor and front-end syntax.


Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants