Wojciech Nawrocki
9b595649bf
hack: rm JavaScript snippet
2022-08-06 11:54:44 -07:00
Wojciech Nawrocki
72b9ba0dc5
chore: move tutorial to examples folder
2022-08-06 11:54:44 -07:00
Wojciech Nawrocki
4e2b3b8345
doc: move widgets chapter to Lean file
2022-08-06 11:54:44 -07:00
Wojciech Nawrocki
273bc683b9
feat: widget tutorial and general RequestM lifts
2022-08-06 11:54:44 -07:00
Mario Carneiro
df85fee62c
chore: rename ac_refl to ac_rfl
2022-08-01 06:53:08 -07:00
Mario Carneiro
d92948bc20
chore: prune ancient keywords
2022-08-01 13:32:56 +02:00
Wojciech Nawrocki
161ef7a67c
doc: fix link
2022-08-01 13:03:54 +02:00
Leonardo de Moura
d38fca5f4d
chore: update phoas.lean
...
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/PHOAS.20example/near/291433426
2022-07-30 08:44:18 -07:00
Leonardo de Moura
3dfa895bf0
feat: OfNat instance postprocessor
...
Closes #1389
2022-07-30 08:35:45 -07:00
E.W.Ayers
591b218607
doc: fix @kha issues
2022-07-25 08:01:27 -07:00
E.W.Ayers
839956c75e
doc: update widget docs
...
[skip ci]
2022-07-25 08:01:27 -07:00
E.W.Ayers
b7d70877f7
feat: user widgets
...
See #1225
2022-07-25 08:01:27 -07:00
Sebastian Ullrich
5160cb7b0f
refactor: remove some unnecessary antiquotation kind annotations
2022-07-23 17:09:32 +02:00
Sebastian Ullrich
9e9786203f
doc: fix minted example
2022-07-23 15:14:44 +02:00
Leonardo de Moura
6d17e8abbf
chore: ICERM notation demo
2022-07-21 08:13:20 -04:00
Leonardo de Moura
977329ce1c
chore: ICERM examples
2022-07-21 06:49:47 -04:00
Yuri de Wit
dc8e404d15
chore: renamed constant to opaque
2022-07-20 15:35:40 -07:00
Sebastian Ullrich
be11e8e29b
doc: missing linebreak
2022-07-18 22:31:16 +02:00
Leonardo de Moura
2116f69315
chore: unused variables
2022-07-17 13:04:08 -04:00
Sebastian Ullrich
6bf7648941
doc: spurious space
2022-07-16 14:51:16 +02:00
Sebastian Ullrich
392c72db86
chore: Nix: renderLean/renderDir
2022-07-15 18:44:17 +02:00
Leonardo de Moura
20d6b9c4aa
doc: add new example
2022-07-09 17:04:08 -07:00
Sebastian Ullrich
6d1b2094e9
chore: nix flake update
...
This comes with ccache 4.6.1, which seems to fix the specific
miscompilation I managed to reproduce with 4.6.0
2022-07-08 13:46:57 +02:00
Leonardo de Moura
fce7697151
fix: def _root_ and dotted notation in recursive definitions
...
closes #1289
2022-07-07 07:57:51 -07:00
Leonardo de Moura
2494f1d4a4
chore: fix doc
2022-07-06 19:56:25 -07:00
Sebastian Ullrich
5e46c0865e
doc: update LeanInk
2022-07-03 17:56:51 +02:00
kzvi
7326c817d2
fix: fix typos in deBruijn.lean and phoas.lean examples
2022-07-02 16:12:05 -07:00
Leonardo de Moura
e81a847ba3
fix: doc/array.md
2022-07-02 15:36:01 -07:00
Timo
e49a81bb56
doc: fix typo
2022-06-27 19:48:45 -07:00
Sebastian Ullrich
ab08bffbec
chore: Nix: fix stage0-from-input
2022-06-27 22:37:02 +02:00
Connor Baker
c213e0e880
doc: fix overwide view when using Alectryon
2022-06-23 18:23:28 +02:00
Sebastian Ullrich
1712d0fee3
chore: update LeanInk
...
Resolves leanprover/LeanInk#20
2022-06-23 11:32:16 +02:00
Sebastian Ullrich
8aea00213c
chore: clean up doc/flake.nix
2022-06-18 13:21:02 +02:00
Sebastian Ullrich
7a3ee51d05
doc: missing word
2022-06-16 10:12:07 +02:00
Leonardo de Moura
5896e6f1d6
chore: fix docs
2022-06-14 17:35:33 -07:00
Leonardo de Moura
97e689d670
chore: add link from Lean 4 manual to FP in Lean
2022-06-09 16:28:54 -07:00
Sebastian Ullrich
388ed62858
chore: update Alectryon
2022-06-07 17:14:41 +02:00
Chris Lovett
885deec745
doc: add link to short quickstart video
2022-06-06 18:32:11 -07:00
Sebastian Ullrich
3cfbdd134a
fix: update Alectryon
2022-06-03 16:05:59 +02:00
larsk21
cf4e106304
fix: unused variables linter review comments
...
- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
2022-06-03 13:03:52 +02:00
larsk21
393fdef972
fix: disable linters in tests
2022-06-03 13:03:52 +02:00
Sebastian Ullrich
4a1885f997
chore: update benchmark suite
2022-05-25 18:26:36 +02:00
Leonardo de Moura
cb32681978
doc: add slide headers to examples
2022-05-23 18:20:37 -07:00
Leonardo de Moura
bf5f107e74
doc: missing NFM examples
2022-05-23 18:04:03 -07:00
Leonardo de Moura
6ce6b12707
doc: NFM'22 examples
2022-05-22 19:21:30 -07:00
Sebastian Ullrich
d13fac6f45
doc: update quickstart
2022-05-18 17:43:14 +02:00
William Blake
9c72917f5e
doc: fix typo gree -> tree
2022-05-09 09:44:48 +02:00
Sebastian Ullrich
f6e74c677e
doc: metaprogramming-arith: deduplicate
2022-05-03 18:38:36 +02:00
Sebastian Ullrich
87431da7b1
doc: metaprogramming-arith: style
2022-05-03 18:38:36 +02:00
Vincent de Haan
20e16f1c75
doc: add amssymb package to latex example to make it work in all cases
2022-04-28 11:21:12 +02:00
