Henrik
d805539b34
chore: update toolchain
2023-08-18 11:07:52 +02:00
Eric Wieser
d3d67c1d92
Do the same for inductives
2023-08-18 11:00:32 +02:00
Eric Wieser
e5ff71991d
Put field docstrings after the field
2023-08-18 11:00:32 +02:00
Henrik
718b182a31
feat: more declaration data as JSON
2023-08-06 15:36:43 +02:00
Henrik
e09280bb3c
feat: order instances and make them unique in their listing
2023-07-31 20:42:30 +02:00
Calvin Lee
75d06a8153
hide color-changer if javascript is disabled
2023-06-09 23:39:59 +02:00
Calvin Lee
cc552ed570
add colorscheme toggle
2023-06-09 23:39:59 +02:00
Alex J. Best
306959b921
feat: list instances for defs also
2023-05-24 01:17:44 +02:00
Henrik
cf86cb4815
feat: attempt to source link directory dependencies
2023-04-24 00:18:29 +02:00
Henrik Böving
9b028566ec
fix: get rid off deleted attribute
2023-04-16 09:54:48 +02:00
Henrik Böving
b9421b9a12
fix: Use Z(separator) instead of S(ymbol) category
...
closes : #123
2023-03-27 15:38:49 +02:00
Henrik Böving
628ef2878e
fix: properly comment out for the workaround
2023-03-16 20:39:30 +01:00
F. G. Dorais
5ab7d0bdd8
fix: unicode dependency
2023-03-15 11:54:57 +01:00
Henrik Böving
0c415232cd
feat: new CI setup
2023-03-12 13:19:02 +01:00
F. G. Dorais
755f06fb0d
fix: correct character category testing
2023-03-11 21:14:36 +01:00
Henrik Böving
5f59fbaac4
refactor: switch to maintained unicode lib
2023-03-11 18:06:32 +01:00
Henrik Böving
720e1acf81
feat: show versions in index HTML
2023-03-09 21:46:38 +01:00
Max Taldykin
c3faad1730
help break_within to split names at `.`
2023-03-04 12:47:30 +01:00
Henrik Böving
5ab6766eb1
fix : #113
2023-02-16 19:51:35 +01:00
Jeremy Salwen
1cb84f6d74
Add filters for search results based on kind.
...
This allows you to search defs, theorems, etc independently.
2023-02-01 15:15:45 +01:00
Henrik Böving
1c44e861be
fix: search.html for relative roots
2023-01-29 14:07:21 +01:00
Jeremy Salwen
3a977a94ca
Fix issues with Search page impelementation
...
- Makes the autocomplete results highlight with up/down arrows.
- Allows you to unselect autocomplete results by using arrow keys.
- Fixed a bug in previous commits where enter did not take you to autocomplete result.
- Return now goes to the search page if no autocomplete result is selected.
- Search results table now properly wraps. (It would be nice to make it wider but I wasn't able to).
- Fixed a bug in the previous commit where docs were not showing, due to failure to copy a modified js file.
2023-01-28 23:00:53 +01:00
Jeremy Salwen
033003c6cb
Add a search page to the docs.
...
Now instead of clicking the "Google Site Search"' button, the user has the option
of clicking the "Search" button, which will take them to a results page. Currently,
the results are identical to the autocomplete results, but the number of results
is not limited to 30. In the future, more information and search options could
be added to this page to make a more powerful search.
Fixes #107
2023-01-28 23:00:53 +01:00
Henrik Böving
a18b27f4c1
feat: attempt to improve usability of the file tree
2023-01-01 20:21:10 +01:00
Henrik Böving
d5ef8006b7
style: Lean 4 compiler style in LeanInk
2023-01-01 19:53:21 +01:00
Henrik Böving
f74443a673
style: Lean 4 compiler style in output
2023-01-01 19:51:01 +01:00
Henrik Böving
3a5c0db46b
style: refactor process to Lean 4 compiler style
2023-01-01 19:30:28 +01:00
Henrik Böving
a5caefc03f
fix: regression in import names
2023-01-01 18:59:19 +01:00
Seppel3210
03e6572584
fix: mention (a : α) → β a notation in foundational types section
2022-12-23 13:28:57 +01:00
Henrik Böving
345036e800
chore: update toolchain
2022-12-22 16:19:23 +01:00
Henrik Böving
f221bbdcff
fix: save the expansion state of the tree again
2022-12-13 20:01:11 +01:00
Henrik Böving
327fdf0ddd
feat: short names in side bar
2022-12-13 19:37:28 +01:00
Henrik Böving
7009910876
chore: update toolchain
2022-12-03 17:43:12 +01:00
Henrik Böving
5e96952a58
chore: update toolchain
2022-12-02 17:55:27 +01:00
Henrik Böving
72034b0831
feat: linkify builtin types
2022-11-22 21:07:59 +01:00
Henrik Böving
b22818b971
feat: render foundational types info
2022-11-22 21:07:59 +01:00
Henrik Böving
e402ee94b1
feat: look for builtin type instances
2022-11-22 21:07:59 +01:00
Parth Shastri
664a86e08b
fix: minor style improvements
2022-11-06 13:53:23 +01:00
Mario Carneiro
9aef28b16e
chore: update toolchain 10-20 ( #86 )
2022-10-20 19:51:26 +02:00
Henrik Böving
64f627a295
chore: toolchain upgrade ( #82 )
...
Halleluja!
2022-10-05 12:05:58 +02:00
Gabriel Ebner
9dc1889de6
chore: update toolchain
2022-08-18 11:33:49 +02:00
Henrik Böving
23ddabb0da
Merge branch 'main' into LeanInkLink
2022-08-11 23:51:26 +02:00
Henrik Böving
d43b23ec9f
fix: Dont linkify unknown names
2022-08-11 23:35:43 +02:00
Henrik Böving
cdfd8ff49c
feat: implement facet
2022-08-11 22:58:25 +02:00
Henrik Böving
6534a71cca
chore: update toolchain
2022-08-11 18:30:28 +02:00
Henrik Böving
d29e14a26a
chore: update toolchain and dependencies
2022-08-09 23:30:43 +02:00
Henrik Böving
5bae061b54
fix: mess of monad transformers in LeanInk adapter
2022-07-27 20:11:41 +02:00
Henrik Böving
108d36d0f0
fix: whitespace after declaration without arguments
...
Closes : #76
2022-07-27 14:19:40 +02:00
Henrik Böving
0ac64f0873
types, types everywhere
2022-07-26 16:26:16 +02:00
Henrik Böving
14afcdbeaf
feat: Degrade --ink to flag
2022-07-26 13:56:22 +02:00