max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
25017 commits 1 branch 0 tags 5.3 GiB
Commit graph

6716 commits

Author SHA1 Message Date
Leonardo de Moura
f816e6107b fix: report (pending) type mismatch errors in simp arguments 2021-06-16 11:35:49 -10:00
Daniel Selsam
51d26e1172 feat: unexpanders take priority 2021-06-13 09:33:49 +02:00
Daniel Selsam
ded51882a0
feat: pp motives and misc delab fixes 2021-06-13 00:06:27 +02:00
Sebastian Ullrich
27d52a352f fix: leanpkg: actually detect import cycles 2021-06-12 10:09:55 +02:00
Sebastian Ullrich
2091a09fa1 feat: IO.Process.Child.takeStdin 2021-06-11 17:53:51 -07:00
Sebastian Ullrich
4ed66cae3e feat: add --print-prefix, --print-libdir flags 
The names were taken from `llvm-config`
 2021-06-11 17:53:51 -07:00
Sebastian Ullrich
1ebcf76d48 refactor: remove explicitly lifted IO functions and move more things into IO.FS 
Automatic lifting takes care of this, and it wasn't consistently applied anyway
 2021-06-11 17:53:51 -07:00
Leonardo de Moura
a435f3d641 feat: reduce s.1 =?= v to s =?= ⟨v⟩ if structure has a single field 
This feature was suggested by @dselsam at PR #521.
It closes #509
 2021-06-11 11:23:19 -07:00
Gabriel Ebner
94e299a730 fix: instantiate mvars in rewrite tactic 2021-06-11 10:27:05 -07:00
Sebastian Ullrich
e4bf5977d9 fix: syntax pattern match against multiple identifiers 2021-06-10 18:15:40 +02:00
Reijo Jaakkola
32897440dc
fix: change IO.FS.Handle.read to return empty array at EOF 
Make EOF handling in IO.FS.Handle consistent with EOF handling in
IO.FS.Handle.getLine. Previously returned error at EOF which ended up
causing segmentation fault. Remove the declaration of g_io_error_eof,
since it becomes redundant.

Closes #349
 2021-06-08 13:17:53 +02:00
Gabriel Ebner
f5f9be191b fix: show expected type in term goal 2021-06-07 16:23:22 -07:00
Gabriel Ebner
5786f58738 feat: plain term goal request 2021-06-07 16:23:22 -07:00
Daniel Fabian
63d58c2f64 refactor: use Except instead of Option in the JSON code. 2021-06-07 12:10:10 +02:00
Daniel Fabian
9200de01ef refactor: fix code review comments. 2021-06-06 06:40:09 -07:00
Daniel Fabian
968ae18f20 fix: deal with params for inductive predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
b7ecc1acc3 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
 2021-06-06 06:40:09 -07:00
Daniel Fabian
822c551aa2 test: Add a bunch of test for structural recursion on predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
ec6f7d9bd6 feat: Implement structural recursion for inductive predicates. 2021-06-06 06:40:09 -07:00
Daniel Fabian
4b7cb058d3 feat: Add support for inductive types to FromJson and ToJson handlers. 2021-06-05 13:53:10 +02:00
Gabriel Ebner
501c31da4d feat: send $/lean/fileProgress notification 2021-06-05 13:49:28 +02:00
Daniel Fabian
06d1d3ae07 fix: Use UInt64 in deriving handler for Hashable. 2021-06-03 06:38:44 -07:00
Leonardo de Moura
995136d46b chore: fix test 2021-06-02 10:03:12 -07:00
Leonardo de Moura
3499016895 chore: improve error message when compiling code containing axioms or noncomputable definitions 
closes #496
 2021-05-31 20:27:15 -07:00
Leonardo de Moura
fb9c1913d7 feat: prototype for equality theorem generator for auxiliary match functions 2021-05-31 18:52:22 -07:00
Leonardo de Moura
4062dee864 fix: fixes #498 2021-05-31 15:42:13 -07:00
Sebastian Ullrich
6857076df4 feat: leanpkg build without external dependencies 2021-05-30 17:29:54 +02:00
Sebastian Ullrich
619873c842 feat: make System.FilePath opaque 2021-05-28 14:19:59 +02:00
Sebastian Ullrich
4354534fda feat: make FilePath a concrete type 
Resolves #363
 2021-05-28 14:19:59 +02:00
Leonardo de Moura
a247249880 feat: add configuration option for disabling proof irrelevance at MetaM 2021-05-27 13:37:26 -07:00
Leonardo de Moura
773dcf3f2e fix: skippingBinders 
This method was assuming the arguments of a `match` auxiliary
application were lambdas. This is not true for the automatically
generated equation theorems.
 2021-05-26 20:09:12 -07:00
Sebastian Ullrich
2988897cac feat: IO.FS.readDir 2021-05-26 09:47:43 +02:00
Wojciech Nawrocki
18e6f78089
fix: publish header processing message log 2021-05-26 09:30:29 +02:00
Sebastian Ullrich
e918e39ed0 feat: have: remove unnecessary whitespace check and allow name- and type-less have 2021-05-25 14:25:14 +02:00
Leonardo de Moura
b91e22af2b fix: fixes #241 2021-05-22 19:10:07 -07:00
Daniel Fabian
c426a816a1 refactor: Make the non-below version of a premise in the below type for inductive predicates implicit. 
Since it is always fully implied by the below version thereof, it carries no real information and shouldn't be used in pattern matching.
 2021-05-22 18:09:32 -07:00
Leonardo de Moura
28b055463f fix: fixes #471 2021-05-22 15:42:52 -07:00
Leonardo de Moura
edb203ca54 fix: fixes #481 2021-05-21 20:40:26 -07:00
Leonardo de Moura
af4485f40e fix: fixes #482 2021-05-21 19:20:24 -07:00
Leonardo de Moura
8eceb07caf feat: new discriminant refinement procedure 2021-05-21 18:08:11 -07:00
Sebastian Ullrich
93327e2324 fix: tactic state on {/· 2021-05-21 17:13:33 -07:00
Sebastian Ullrich
e257caa446 feat: move block tactic macro to Init 2021-05-21 17:13:33 -07:00
Mac Malone
a6dc9e4ef3 feat: class abbrev now supports a type spec (+ test) 2021-05-20 15:23:30 -07:00
Mac Malone
6c07536b33 feat: simplified, improved class abbrev (+ tests) 2021-05-20 15:23:29 -07:00
Daniel Fabian
42bd44ab82 refactor: Capture environment modification in mkMatcher. 
Doing this allows us to add the declaration in the backtracking case of structural recursion.
 2021-05-20 15:20:16 -07:00
Sebastian Ullrich
9f3ddb0c43 fix: do not store solved goals in info tree 2021-05-20 15:17:54 -07:00
Sebastian Ullrich
a02c6fd3eb chore: adapt stdlib & tests 2021-05-20 15:17:36 -07:00
Sebastian Ullrich
7242c5c513 fix: rw: add all uninstantiated mvars as goals 2021-05-19 07:31:50 -07:00
Daniel Fabian
ab0ef229ac feat: add getBelowIndices. 2021-05-19 07:28:14 -07:00
Daniel Fabian
91ecbb5b5c feat: Add withMkMatcherInput. 
This is the inverse function to `mkMatcher`, i.e. a way to turn a matcher into an input.
 2021-05-19 07:28:14 -07:00