| "Foo structure is just a test " | |
| "main name " | |
| "documentation for the second field " | |
| "documenting test axiom " | |
| doc string for 'Boo' is not available | |
| "Boo constructor has a custom name " | |
| "Boo.x docString " | |
| doc string for 'Boo.y' is not available | |
| "inductive datatype Tree documentation " | |
| "Tree.node documentation " | |
| "Tree.leaf stores the values " | |
| "documenting definition in namespace " | |
| "We can document 'where' functions too\n\n... and indentation is stripped, even after an empty line. " | |
| doc string for 'f' is not available | |
| "let rec documentation at f " | |
| doc string for 'g' is not available | |
| "let rec documentation at g " | |
| "Gadget for optional parameter support.\n\nA binder like `(x : α := default)` in a declaration is syntax sugar for\n`x : optParam α default`, and triggers the elaborator to attempt to use\n`default` to supply the argument if it is not supplied.\n" | |
| "Auxiliary declaration used to implement named patterns like `x@h:p`. " | |
| "Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\nit reduces `A` and continues building the telescope if it is a `forall`.\n\nIf `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.\n" | |
| Foo := | |
| { range := { pos := { line := 3, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 6, column := 58 }, | |
| endCharUtf16 := 58 }, | |
| selectionRange := { pos := { line := 4, column := 10 }, | |
| charUtf16 := 10, | |
| endPos := { line := 4, column := 13 }, | |
| endCharUtf16 := 13 } } | |
| Foo.name := | |
| { range := { pos := { line := 5, column := 19 }, | |
| charUtf16 := 19, | |
| endPos := { line := 5, column := 23 }, | |
| endCharUtf16 := 23 }, | |
| selectionRange := { pos := { line := 5, column := 19 }, | |
| charUtf16 := 19, | |
| endPos := { line := 5, column := 23 }, | |
| endCharUtf16 := 23 } } | |
| Foo.val := | |
| { range := { pos := { line := 6, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 6, column := 47 }, | |
| endCharUtf16 := 47 }, | |
| selectionRange := { pos := { line := 6, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 6, column := 47 }, | |
| endCharUtf16 := 47 } } | |
| myAxiom := | |
| { range := { pos := { line := 8, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 9, column := 19 }, | |
| endCharUtf16 := 19 }, | |
| selectionRange := { pos := { line := 9, column := 6 }, | |
| charUtf16 := 6, | |
| endPos := { line := 9, column := 13 }, | |
| endCharUtf16 := 13 } } | |
| Boo := | |
| { range := { pos := { line := 11, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 15, column := 12 }, | |
| endCharUtf16 := 12 }, | |
| selectionRange := { pos := { line := 11, column := 10 }, | |
| charUtf16 := 10, | |
| endPos := { line := 11, column := 13 }, | |
| endCharUtf16 := 13 } } | |
| Boo.makeBoo := | |
| { range := { pos := { line := 13, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 13, column := 9 }, | |
| endCharUtf16 := 9 }, | |
| selectionRange := { pos := { line := 13, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 13, column := 9 }, | |
| endCharUtf16 := 9 } } | |
| Boo.x := | |
| { range := { pos := { line := 14, column := 27 }, | |
| charUtf16 := 27, | |
| endPos := { line := 14, column := 28 }, | |
| endCharUtf16 := 28 }, | |
| selectionRange := { pos := { line := 14, column := 27 }, | |
| charUtf16 := 27, | |
| endPos := { line := 14, column := 28 }, | |
| endCharUtf16 := 28 } } | |
| Boo.y := | |
| { range := { pos := { line := 15, column := 4 }, | |
| charUtf16 := 4, | |
| endPos := { line := 15, column := 5 }, | |
| endCharUtf16 := 5 }, | |
| selectionRange := { pos := { line := 15, column := 4 }, | |
| charUtf16 := 4, | |
| endPos := { line := 15, column := 5 }, | |
| endCharUtf16 := 5 } } | |
| Tree := | |
| { range := { pos := { line := 17, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 20, column := 56 }, | |
| endCharUtf16 := 56 }, | |
| selectionRange := { pos := { line := 18, column := 10 }, | |
| charUtf16 := 10, | |
| endPos := { line := 18, column := 14 }, | |
| endCharUtf16 := 14 } } | |
| Tree.rec := | |
| { range := { pos := { line := 17, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 20, column := 56 }, | |
| endCharUtf16 := 56 }, | |
| selectionRange := { pos := { line := 18, column := 10 }, | |
| charUtf16 := 10, | |
| endPos := { line := 18, column := 14 }, | |
| endCharUtf16 := 14 } } | |
| Tree.casesOn := | |
| { range := { pos := { line := 17, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 20, column := 56 }, | |
| endCharUtf16 := 56 }, | |
| selectionRange := { pos := { line := 18, column := 10 }, | |
| charUtf16 := 10, | |
| endPos := { line := 18, column := 14 }, | |
| endCharUtf16 := 14 } } | |
| Tree.node := | |
| { range := { pos := { line := 19, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 19, column := 64 }, | |
| endCharUtf16 := 64 }, | |
| selectionRange := { pos := { line := 19, column := 35 }, | |
| charUtf16 := 35, | |
| endPos := { line := 19, column := 39 }, | |
| endCharUtf16 := 39 } } | |
| Tree.leaf := | |
| { range := { pos := { line := 20, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 20, column := 56 }, | |
| endCharUtf16 := 56 }, | |
| selectionRange := { pos := { line := 20, column := 39 }, | |
| charUtf16 := 39, | |
| endPos := { line := 20, column := 43 }, | |
| endCharUtf16 := 43 } } | |
| Bla.test := | |
| { range := { pos := { line := 24, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 31, column := 16 }, | |
| endCharUtf16 := 16 }, | |
| selectionRange := { pos := { line := 25, column := 4 }, | |
| charUtf16 := 4, | |
| endPos := { line := 25, column := 8 }, | |
| endCharUtf16 := 8 } } | |
| Bla.test.aux := | |
| { range := { pos := { line := 31, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 31, column := 16 }, | |
| endCharUtf16 := 16 }, | |
| selectionRange := { pos := { line := 31, column := 2 }, | |
| charUtf16 := 2, | |
| endPos := { line := 31, column := 5 }, | |
| endCharUtf16 := 5 } } | |
| f := | |
| { range := { pos := { line := 35, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 39, column := 14 }, | |
| endCharUtf16 := 14 }, | |
| selectionRange := { pos := { line := 35, column := 4 }, | |
| charUtf16 := 4, | |
| endPos := { line := 35, column := 5 }, | |
| endCharUtf16 := 5 } } | |
| f.foo := | |
| { range := { pos := { line := 36, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 38, column := 22 }, | |
| endCharUtf16 := 22 }, | |
| selectionRange := { pos := { line := 36, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 36, column := 47 }, | |
| endCharUtf16 := 47 } } | |
| g := | |
| { range := { pos := { line := 41, column := 0 }, | |
| charUtf16 := 0, | |
| endPos := { line := 45, column := 7 }, | |
| endCharUtf16 := 7 }, | |
| selectionRange := { pos := { line := 41, column := 4 }, | |
| charUtf16 := 4, | |
| endPos := { line := 41, column := 5 }, | |
| endCharUtf16 := 5 } } | |
| g.foo := | |
| { range := { pos := { line := 42, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 44, column := 22 }, | |
| endCharUtf16 := 22 }, | |
| selectionRange := { pos := { line := 42, column := 44 }, | |
| charUtf16 := 44, | |
| endPos := { line := 42, column := 47 }, | |
| endCharUtf16 := 47 } } | |
| docStr.lean:106:0-107:20: error: invalid 'add_decl_doc', declaration is in an imported module |