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

fix: delaborating projections

Browse source
This commit is contained in:
Sebastian Ullrich 2020-09-17 13:50:43 +02:00 • committed by Leonardo de Moura
parent c4761974b7
commit 6a91fb1613
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Delaborator.lean
View file

@ -520,7 +520,8 @@ e ← withProj delab;
-- not perfectly authentic: elaborates to the `idx`-th named projection
-- function (e.g. `e.1` is `Prod.fst e`), which unfolds to the actual
-- `proj`.
`($(e).$(mkStxNumLitAux idx):fieldIdx)
let idx := mkStxLit fieldIdxKind (toString (idx + 1));
`($(e).$idx:fieldIdx)
/-- Delaborate a call to a projection function such as `Prod.fst`. -/
@[builtinDelab app]