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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2022-01-17 17:24:09 -08:00
parent 4ac019ccf0
commit b266961068
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/docStr.lean.expected.out
View file

@ -16,7 +16,7 @@ doc string for 'f' is not available
doc string for 'g' is not available
"let rec documentation at g "
"Gadget for optional parameter support. "
"Auxiliary Declaration used to implement the named patterns `x@p`\n -- TODO: add proof for `x = a`\n"
"Auxiliary Declaration used to implement the named patterns `x@h:p` "
"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\n it reduces `A` and continues bulding the telescope if it is a `forall`. "
Foo :=
{ range := { pos := { line := 4, column := 0 },