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

doc: fix misleading SubExpr docstring

Browse source
This commit is contained in:
E.W.Ayers 2022-06-03 16:25:21 -04:00 • committed by Leonardo de Moura
parent d00d8a2104
commit d55daf80d4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/SubExpr.lean
View file

@ -15,8 +15,8 @@ abbrev SubExpr.Pos := Nat
/-- An expression and the position of a subexpression within this expression.
Subexpressions are encoded as the parent root expression `e` and a
position `p : Pos` denoting a particular subexpression in `e`.
Subexpressions are encoded as the current subexpression `e` and a
position `p : Pos` denoting `e`'s position with respect to the root expression.
We use a simple encoding scheme for expression positions `Pos`:
every `Expr` constructor has at most 3 direct expression children. Considering an expression's type