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
Leonardo de Moura
feb71271e9
fix: remove redundant alternatives
2022-07-31 05:28:14 -07:00
Leonardo de Moura
fbc6bcff92
chore: remove unnecessary french quotes
2022-07-29 20:53:01 -07:00
Leonardo de Moura
eafd2a88ce
chore: simplify Prelude.lean and Core.lean using elabAsElim
2022-07-29 18:13:56 -07:00
Sebastian Ullrich
f1f0f60768
fix: linter warnings
2022-07-29 10:31:19 -07:00
Ed Ayers
c3f58a7eab
feat: add a message if Lean 4 is called with the Lean 3 extension
2022-07-29 11:08:51 +00:00
Leonardo de Moura
012cb13f51
feat: add [elabAsElim] elaboration strategy
2022-07-28 20:08:29 -07:00
Leonardo de Moura
ee6e2036dd
feat: allow relations in Type at Trans
...
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Calc.20mode/near/291214574
2022-07-28 10:13:01 -07:00
Leonardo de Moura
1c770ac8d7
feat: doc strings for declare_syntax_cat
...
see #1374
2022-07-27 13:40:08 -07:00
Leonardo de Moura
3363ee414b
doc: add doc strings for declarations added by the init_quot command
...
See #1374
2022-07-27 10:17:03 -07:00
Leonardo de Moura
97a5a88ae2
doc: add doc string to simp attribute parser
2022-07-27 06:34:55 -07:00
Leonardo de Moura
bbad6d1efe
feat: add with_annotate_term
2022-07-26 15:13:28 -07:00
Leonardo de Moura
f1f5a4b39e
chore: naming convention
2022-07-24 17:44:29 -07:00
Leonardo de Moura
5e877b115b
feat: improve calc tactic
...
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.
Closes #1342
2022-07-24 14:30:15 -07:00
Leonardo de Moura
c46ef56ac7
perf: avoid blowup at deriving Repr
...
The fix is not perfect. I just avoided inlining in some builtin `Repr` instances.
The actual problem is at `ElimDeadBranches.lean`.
Closes #1365
2022-07-24 13:10:04 -07:00
