Leonardo de Moura
82ae779218
fix: missing test at addDocString ( #3823 )
...
closes #3497
2024-04-02 02:29:14 +00:00
Scott Morrison
94d6286e5a
chore: reorganising to reduce imports ( #3790 )
...
[Before](https://github.com/leanprover/lean4/files/14772220/oi.pdf ) and
[after](https://github.com/leanprover/lean4/files/14772226/oi2.pdf ).
This gets `ByteArray`, `String.Extra`, `ToString.Macro` and `RCases` out
of the imports of `omega`. I'd hoped to get `Array.Subarray` too, but
it's tangled up in the list literal syntax. Further progress could come
from make `split` use available `Decidable` instances, so we could pull
out `Classical` (and possibly some of `PropLemmas`).
2024-03-27 11:15:01 +00:00
Joe Hendrix
29244f32f6
chore: upstream solve_by_elim ( #3408 )
...
This upstreams the solve_by_elim tactic from Std.
It is a key tactic needed by library_search.
2024-02-21 01:16:04 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Joachim Breitner
368ead54b2
refactor: termination_by changes in stdlib
2024-01-10 17:27:35 +01:00
Mario Carneiro
391aef5cd7
feat: automatic extension names
2022-10-06 17:19:30 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Gabriel Ebner
ed9b5bcb92
fix: make all syntax accessors non-panicking
2022-09-14 10:17:00 -07:00
Gabriel Ebner
b4af14d44a
fix: deindent docstrings with empty lines
2022-09-13 07:16:12 -07:00
Leonardo de Moura
a2631ce037
fix: panic when Syntax.missing
...
I got a panic error message today in VS Code because of this function.
It is weird because, as far as I can tell, this function is only used by
the `register_simp_attr` macro, and this macro was not being used in
the files I was editing.
I think the fix is resonable for a `Syntax.missing` case.
cc @gebner
2022-09-12 16:10:14 -07:00
Gabriel Ebner
fb259f95db
feat: remove description argument from register_simp_attr
2022-09-08 14:49:43 -07:00
Sebastian Ullrich
fb408c024b
fix: deleting built-in docstrings
2022-08-27 17:19:25 +02:00
Leonardo de Moura
a30a31b1b0
fix: findDocString?
2022-08-04 10:32:41 -07:00
Leonardo de Moura
92d360353c
feat: elaborate add_decl_doc
2022-07-27 09:58:49 -07:00
Leonardo de Moura
2c0de29dfd
feat: add add_decl_doc command
2022-07-27 09:30:32 -07:00
Leonardo de Moura
c341d8432f
feat: remove leading spaces from docstrings
2022-07-18 22:18:15 -04:00
Xubai Wang
ca521e1188
feat: add position to mod doc
2022-02-16 13:50:19 -08:00
Leonardo de Moura
12e2a79170
chore: fix codebase after removing auto pure
2022-02-03 18:08:14 -08:00
Sebastian Ullrich
e9f7c88299
feat: record doc strings of builtin parsers & elaborators
2021-11-26 17:13:19 +01:00
Leonardo de Moura
6a880fecc9
chore: modify findDocString?
2021-09-21 17:29:40 -07:00
Leonardo de Moura
3d485bf375
feat: add moduleDocExt
2021-08-06 13:40:54 -07:00
Leonardo de Moura
84f78edb31
feat: store declaration ranges
2021-01-11 12:50:11 -08:00
Leonardo de Moura
c4259649ed
refactor: add MapDeclarationExtension
2021-01-10 18:25:56 -08:00
Leonardo de Moura
308c61027a
feat: save doc strings
...
We can now document `let rec` too.
2021-01-10 07:13:33 -08:00
Leonardo de Moura
2c8001a7f3
feat: add DocString.lean
2021-01-10 07:13:33 -08:00
