max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: do not discriminate anonymous antiquots after all

Browse source
This commit is contained in:
Sebastian Ullrich 2022-04-28 22:39:52 +02:00
parent 9b71fbb461
commit 4b78d02a5e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/Quotation.lean
View file

@ -323,7 +323,7 @@ private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo :=
-- let id := stx; let e := stx; ...
-- else
-- let e := stx; ...
if pseudoKinds.all id then unconditionally rhsFn else pure {
if (getCanonicalAntiquot quoted)[3].isNone || pseudoKinds.all id then unconditionally rhsFn else pure {
check := shape ks none,
onMatch := fun
| other _ => undecided