Leonardo de Moura
bdea43a52a
feat: while and repeat macros
2022-02-24 16:26:07 -08:00
Leonardo de Moura
f7f04483b1
feat: add src/Lean/Meta/Tactic/LinearArith/Nat.lean
2022-02-24 15:24:59 -08:00
Leonardo de Moura
bd3ad35a1c
fix: we may get False in unreachable branches
2022-02-24 15:24:07 -08:00
Leonardo de Moura
8131aa5a64
chore: add simp theorem heq_eq_eq
2022-02-24 13:45:34 -08:00
Leonardo de Moura
b134b9a3a4
chore: move isNatProjInst
2022-02-24 13:45:34 -08:00
Leonardo de Moura
a430b2ad71
chore: add copyright
2022-02-24 13:45:34 -08:00
Leonardo de Moura
05be43455a
feat: add src/Init/Data/Nat/Linear.lean
2022-02-24 13:45:17 -08:00
Leonardo de Moura
43c2169f78
fix: when performing contextual simplification, and arrow may become a dependent arrow
...
fixes #1024
2022-02-23 18:43:32 -08:00
Leonardo de Moura
49c64040a2
feat: add support for HEq at injections tactic
2022-02-23 17:31:17 -08:00
Leonardo de Moura
07d1ec1926
fix: simp_all was "self-simplifying" simplified hypotheses
...
fixes #1027
2022-02-23 16:48:28 -08:00
Leonardo de Moura
0125db40a2
fix: remove [..] annotation from if simp theorems
...
fixes #1025
2022-02-23 16:28:12 -08:00
Leonardo de Moura
3e0ea7fbae
fix: use instantiateMVars before invoking pure function findIfToSplit
2022-02-23 16:25:33 -08:00
Leonardo de Moura
a1366fcb3b
chore: cleanup
2022-02-23 16:24:42 -08:00
Leonardo de Moura
c491659970
feat: improve split tactic error message
2022-02-23 16:00:42 -08:00
Leonardo de Moura
902e60c480
feat: add Format.isEmpty
2022-02-23 13:34:25 -08:00
Leonardo de Moura
52b53ab7a2
fix: heuristic for generating equation theorem types
...
closes #1026
2022-02-23 13:10:30 -08:00
Leonardo de Moura
2340f1b9bd
feat: add isBRecOnRecursor
2022-02-23 13:09:29 -08:00
Leonardo de Moura
15546fbc48
feat: add Expr.findExt?
2022-02-23 12:32:17 -08:00
Leonardo de Moura
dbe9bf61c5
fix: unfold auxiliary theorems created by decreasing_tactic
2022-02-23 09:02:23 -08:00
Leonardo de Moura
4794b9709f
feat: improve equation theorem and match-splitter generation at MatchEqns.lean
2022-02-22 17:43:42 -08:00
Leonardo de Moura
52ff840321
feat: support for HEq at injection
2022-02-22 17:24:11 -08:00
Leonardo de Moura
c9f8ec71df
fix: invalid rewrite when proving equation theorems for declaration using well-founded recursion
2022-02-22 16:38:51 -08:00
Leonardo de Moura
24249fecd3
feat: helper simp theorems
2022-02-22 16:03:36 -08:00
Leonardo de Moura
8d6750469e
chore: helper Nat theorems
2022-02-22 14:26:50 -08:00
Leonardo de Moura
c73d177c94
perf: simpH? at MatchEqns.lean
2022-02-21 12:04:03 -08:00
Leonardo de Moura
0e40c63292
chore: fix typo
2022-02-21 10:55:38 -08:00
Leonardo de Moura
7f3a3138d0
feat: helper Nat theorems
2022-02-21 08:49:50 -08:00
Sebastian Ullrich
d39c23f061
feat: quot precheck for →
2022-02-21 10:14:39 +01:00
Leonardo de Moura
33b1d2fd98
fix: preserve arrow binder names and info at simp
...
We use the idiom `revert; simp; ...; intro` in a few places. Some of
the reverted hypotheses manifest themselves as arrows in the target.
Before this commit, `simp` would lose the binder names and info when
simplifying an arrow, and we would get inaccessible names when
reintroducing them.
2022-02-20 16:27:40 -08:00
Leonardo de Moura
ba16903205
feat: add helper theorems
2022-02-19 21:25:44 -08:00
Leonardo de Moura
193859c72c
feat: add helper theorems
2022-02-19 17:53:54 -08:00
Leonardo de Moura
7a81589c49
feat: improve "constant approximation" heuristic used at isDefEq
2022-02-19 08:09:31 -08:00
Leonardo de Moura
19bcb5fb31
feat: add Array.popWhile and Array.takeWhile
2022-02-19 07:04:52 -08:00
Leonardo de Moura
a4d6cbfedd
feat: improve match elaborator
2022-02-19 06:12:21 -08:00
Leonardo de Moura
f64f563936
chore: fix comment
2022-02-19 06:11:53 -08:00
Leonardo de Moura
e61d0be561
feat: isolate fixed prefix at well-founded recursion
...
closes #1017
2022-02-18 10:40:32 -08:00
Leonardo de Moura
75e771b6e8
feat: add support for fixed argument prefix at mkFix and elabWFRel
...
This is needed for #1017
TODO: `addNonRecPreDefs` and equation theorems
2022-02-18 07:59:32 -08:00
Leonardo de Moura
70312191f7
feat: make sure packDomain and packMutual ignore the fixed arguments
...
TODO: adapt `elabWFRel`, `mkFix`, and etc.
This is needed for #1017
2022-02-17 17:43:06 -08:00
Leonardo de Moura
9ee529e5ce
fix: use PSum instead of Sum when using well-founded recursion
...
See new test for example that did not work with `Sum` because type
alpha was `Sort u`.
2022-02-17 16:14:34 -08:00
Leonardo de Moura
4a0ae8326c
feat: compute the fixed prefix size for mutually recursive definitions
2022-02-17 14:12:05 -08:00
Leonardo de Moura
dedb6ee01b
fix: skip value if type is computationally irrelevant
2022-02-17 10:41:16 -08:00
Leonardo de Moura
ba0904060b
chore: missing trace_pp_expr
2022-02-17 10:40:21 -08:00
Leonardo de Moura
4ed5c8405b
feat: improve IR checker error messages
2022-02-17 09:51:05 -08:00
Xubai Wang
ca521e1188
feat: add position to mod doc
2022-02-16 13:50:19 -08:00
Leonardo de Moura
e1d9dc4b38
feat: store noncomputable declarations
2022-02-16 13:33:02 -08:00
Leonardo de Moura
4ba1e0ad4b
feat: add isNoncomputable function for querying whether a given declaration has been marked as "noncomputable" by users
2022-02-16 13:20:31 -08:00
Leonardo de Moura
ad5099ec3c
fix: mkLetRecClosureFor for nested let-recs
...
closes #1020
2022-02-16 12:44:02 -08:00
Leonardo de Moura
86328bcb9f
feat: tail recursive List.iota and [csimp] theorem
2022-02-16 11:25:46 -08:00
Leonardo de Moura
3f4d8f370a
fix: backtrack InfoTree when backtracking at the discriminant refinement method
...
This commit addresses issue described at https://github.com/leanprover/lean4/issues/1018#issuecomment-1040597212
closes #1018
2022-02-15 16:01:09 -08:00
Leonardo de Moura
fd9165415e
feat: try to preserve variable names during discriminant refinement
...
This fixes second issue at #1018
2022-02-15 15:54:03 -08:00
