Mario Carneiro
d875f43b52
chore: remove outdated TODO
2022-08-26 15:31:13 -07:00
Fynn Schmitt-Ulms
064ab16791
feat: Float.abs function ( #1514 )
2022-08-25 18:45:46 -07:00
pcpthm
bc9c14a080
fix: remove duplicate OfNat Int instance
2022-08-25 11:57:13 -07:00
Richard Musiol
d4799eaf3a
doc: fix typo
2022-08-24 21:59:15 -07:00
Sebastian Ullrich
5ce5576b5d
fix: hygienic resolution of namespaces
2022-08-20 22:29:46 +02:00
Sebastian Ullrich
5694dea36d
chore: prepare bootstrap change
2022-08-20 22:29:46 +02:00
Leonardo de Moura
8985a15f96
chore: mark inferInstance and inferInstanceAs as [inline]
...
New code generator does not inline simple declarations not tagged with
`[inline]` yet. We need this change to simpilify testing
2022-08-17 19:08:51 -07:00
Mario Carneiro
20f9b7172f
doc: documentation for Init.SizeOf
2022-08-17 14:48:10 -07:00
Mario Carneiro
8182f83929
doc: documentation for Init.Tactics
2022-08-17 14:44:40 -07:00
E.W.Ayers
4e7c1e1ec8
fix: missing digits in scientific literal should be an error
2022-08-17 05:57:22 -07:00
Mario Carneiro
ba938d4a6e
doc: documentation for Init.Notation
2022-08-17 05:56:10 -07:00
E.W.Ayers
d543867241
doc: fix typos
2022-08-16 08:31:58 -07:00
E.W.Ayers
ff5b02622c
doc: Format
2022-08-16 08:31:58 -07:00
E.W.Ayers
2e99e8c22d
feat: Float ↔ Json
2022-08-16 08:01:23 -07:00
E.W.Ayers
a763d9d81e
fix: decodeScientificLitVal? parses 1.0e+1 correctly
...
fixes #1484
2022-08-16 07:29:39 -07:00
Leonardo de Moura
ef308e7f2c
chore: remove leftover notation
2022-08-15 06:25:35 -07:00
Sebastian Ullrich
a2d59b9c93
fix: preserve condition position info in if
2022-08-13 18:07:30 -07:00
Sebastian Ullrich
a91ad198b2
fix: set ref in expandMacros like with regular expansion
2022-08-13 18:07:30 -07:00
Sebastian Ullrich
b97a145836
fix: annotate all syntax nodes produced by quotations as synthetic
2022-08-13 18:07:30 -07:00
Mario Carneiro
b0db7deeef
doc: documentation for Init.Coe
2022-08-13 17:15:49 -07:00
Mario Carneiro
9de477ecf9
feat: add more float functions
2022-08-12 13:12:59 -07:00
Mario Carneiro
6906a4d1ee
feat: generalize ReaderT definitions
2022-08-12 08:23:11 -07:00
Mario Carneiro
e51d892fc2
feat: implement USize.toUInt64 model
2022-08-09 18:04:05 -07:00
Leonardo de Moura
9e00cbd6d8
feat: add LCNFTypes.lean
2022-08-09 15:47:58 -07:00
Mario Carneiro
a28c19c161
doc: improve typeclass ops documentation
2022-08-09 14:25:44 -07:00
Mario Carneiro
6026894f9f
doc: finish Init.Prelude docs
2022-08-09 14:25:44 -07:00
Leonardo de Moura
1d9075db0b
chore: add more helper axioms for code generator
2022-08-06 20:20:50 -07:00
Wojciech Nawrocki
9c78f6fa0e
feat: make include_str a builtin
2022-08-06 11:54:44 -07:00
Mario Carneiro
37d3479e7c
doc: add more docs to Init.Prelude
2022-08-06 09:32:16 -07:00
Mario Carneiro
83da649a24
chore: remove typedExpr
2022-08-05 11:42:36 -07:00
Leonardo de Moura
50cecdbb62
chore: add Inhabited MProd and Inhabited PProd instances
...
closes #1420
2022-08-05 11:21:27 -07:00
Leonardo de Moura
fdaae20594
chore: remove workaround
2022-08-04 21:29:31 -07:00
Leonardo de Moura
55bb8e905a
chore: binderIdent normalization
...
fixes #1411
2022-08-04 21:10:02 -07:00
Leonardo de Moura
659300597d
doc: some doc strings for Prelude.lean
2022-08-04 20:55:13 -07:00
Leonardo de Moura
16d6f13eed
chore: fix warnings
2022-08-04 16:05:09 -07:00
Mario Carneiro
f5c5af1e86
doc: document all the syntax categories ( #1401 )
...
* chore: use Category declarations for builtin cats too
* doc: document all the syntax categories
* fix: fix test
2022-08-03 18:13:39 -07:00
Mario Carneiro
e816424466
chore: use Category declarations for builtin cats too ( #1400 )
2022-08-03 18:10:54 -07:00
Leonardo de Moura
e9bcc779fe
feat: add Array.mapM'
2022-08-03 11:18:19 -07:00
Leonardo de Moura
5df588cbbf
chore: remove unnecessary annotations
2022-08-02 05:42:53 -07:00
Sebastian Ullrich
a44472962d
fix: replace uses of token antiquotations in tactics with with_annotate_state
2022-08-02 04:54:48 -07:00
Leonardo de Moura
99413a18ff
feat: add congr tactic
2022-08-01 18:44:07 -07:00
Mario Carneiro
5f39370d94
chore: rename skip conv to rfl and add no-op skip
2022-08-01 13:54:36 -07:00
Leonardo de Moura
8781203372
chore: rename misleading function
...
`charToHex` is an auxiliary function used at `Char.quoteCore` for
converting ASCII control characters into `\x` notation.
Its name was misleading.
Closes #1404
2022-08-01 13:21:03 -07:00
Leonardo de Moura
0156b59ef1
chore: enforce naming convention
2022-08-01 09:58:11 -07:00
Mario Carneiro
f235cd8537
doc: document all the convs
2022-08-01 09:28:30 -07:00
Mario Carneiro
5ed3e580ef
fix: allow {} as conv
2022-08-01 08:47:51 -07:00
Mario Carneiro
25aea1b723
doc: document all the tactics
2022-08-01 08:08:03 -07:00
Mario Carneiro
df85fee62c
chore: rename ac_refl to ac_rfl
2022-08-01 06:53:08 -07:00
Mario Carneiro
c952c69690
feat: add missingDocs linter
2022-07-31 18:18:21 -07:00
Mario Carneiro
42a4f2f451
feat: ForIn instance for NameMap and PersistentHashMap
2022-07-31 15:42:26 -07:00
