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

28057 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
d03f0b3851 fix: set of chained lexical references 2022-05-11 17:32:06 +02:00
Sebastian Ullrich
23fac14b33 chore: try with fresh cache 2022-05-11 12:31:55 +02:00
Leonardo de Moura
94d2a3ef86 feat: improve error message when failing to infer resulting universe level for inductive datatypes and structures 2022-05-10 18:30:53 -07:00
Leonardo de Moura
c935a3ff6a feat: improve error location for universe level errors at inductive command 2022-05-10 12:50:01 -07:00
Sebastian Ullrich
392640d292 feat: allow keyword-like projection identifiers 2022-05-10 12:25:30 -07:00
Leonardo de Moura
37b2f74404 chore: update stage0 2022-05-10 11:24:10 -07:00
Leonardo de Moura
1d066364f3 chore: update stage0 2022-05-10 11:21:54 -07:00
Leonardo de Moura
f58afaaa43 fix: make sure let _ := val and let _ : type := val are treated at letIdDecl 
closes #1114
 2022-05-10 06:52:27 -07:00
Sebastian Ullrich
1b51bab4a1 feat: turn on info trees by default 2022-05-10 06:24:31 -07:00
Leonardo de Moura
7ce0471f28 feat: improve binrel% elaborator 
It now relies on `binop%` too, and addresses issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387
 2022-05-09 18:39:52 -07:00
Leonardo de Moura
1768067aa0 doc: document elaboration issue 
described at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Regression.20in.20coercion.20inference/near/281737387

TODO: improve `binrel%` elaboration function.
 2022-05-09 17:39:24 -07:00
Sebastian Ullrich
ff6537be1b fix: use consistent goal prefix everywhere 2022-05-09 17:49:00 +02:00
Leonardo de Moura
fc03b2fc31 feat: unfold ident,+ 2022-05-09 07:09:53 -07:00
Leonardo de Moura
2680711f6a chore: update stage0 2022-05-09 07:09:53 -07:00
Leonardo de Moura
995d4f0979 chore: prepare for unfold ident,+ 2022-05-09 07:09:22 -07:00
Leonardo de Moura
e729b32b2b feat: unfold should fail if it didn't unfold anything 2022-05-09 06:41:17 -07:00
Leonardo de Moura
4875224bd4 feat: unfold tactic tries to reduce match after unfolding 2022-05-09 06:35:40 -07:00
Leonardo de Moura
ecbc59c8d8 chore: split Notation.lean 2022-05-09 05:20:19 -07:00
Sebastian Ullrich
fa7c35f4f6 doc: normalize tactic doc strings 2022-05-09 10:37:59 +02:00
William Blake
9c72917f5e
doc: fix typo gree -> tree 2022-05-09 09:44:48 +02:00
Leonardo de Moura
3cd46888bf fix: check types using default reducibility at synthInstance? 
closes #1131
 2022-05-08 06:49:14 -07:00
Leonardo de Moura
0fd47fd817 chore: update stage0 2022-05-07 15:52:01 -07:00
Sebastian Ullrich
91991649bc fix: connect occurrences of mutable variable inside and outside for in info tree 2022-05-07 15:50:26 -07:00
Sebastian Ullrich
22f8ea147c fix: propagate position information of variables in do blocks 2022-05-07 15:50:26 -07:00
Sebastian Ullrich
daa9e03e78 fix: combineFvars 2022-05-07 15:50:26 -07:00
Sebastian Ullrich
2f461d201e fix: info tree of let_delayed 2022-05-07 15:50:26 -07:00
François G. Dorais
155b41937a
fix: remove unnecessary hypothesis (#1144) 2022-05-07 15:39:37 -07:00
Leonardo de Moura
9043f91d8c fix: if Tactic.Context.recover == false, we must disable "error to sorry" when elaborating terms in tactics 
closes #1142
 2022-05-07 15:37:12 -07:00
Leonardo de Moura
ab31f9ad5d fix: fixes #1143 2022-05-07 15:27:34 -07:00
Leonardo de Moura
dc1b16c4fb chore: update stage0 2022-05-07 15:10:06 -07:00
Leonardo de Moura
2c8c20d424 feat: add [eliminator] attribute specifying default recursors/eliminators for the cases and induction tactics 2022-05-07 15:09:42 -07:00
Leonardo de Moura
73cb952275 feat: add Hashable (Array α) instance 2022-05-07 15:01:32 -07:00
Leonardo de Moura
b5bcf252ce chore: cleanup 2022-05-07 14:48:22 -07:00
Leonardo de Moura
af5e13e534 feat: improve binop% elaboration function 2022-05-07 10:32:55 -07:00
Leonardo de Moura
38baeaf373 feat: backtrack when applying default instances if subproblems cannot be solved 2022-05-07 09:56:38 -07:00
Leonardo de Moura
8c23bef399 feat: add support for casesOn applications to structural and well-founded recursion modules 2022-05-06 17:12:10 -07:00
Leonardo de Moura
090503cfd5 chore: cleanup 2022-05-06 17:12:10 -07:00
KaseQuark
5ebd6c28db
feat: change "⊢" in conv goals to "|" 2022-05-06 09:35:04 +02:00
Leonardo de Moura
7a1c79043e chore: fix test 2022-05-04 15:34:37 -07:00
Leonardo de Moura
dce92c6362 chore: update stage0 2022-05-04 15:32:22 -07:00
Leonardo de Moura
db89750030 chore: update RELEASES.md 2022-05-04 15:31:57 -07:00
Leonardo de Moura
5aaccc8ebb chore: remove OptionM 2022-05-04 15:30:10 -07:00
Leonardo de Moura
eaea5c4773 chore: update stage0 2022-05-04 15:28:49 -07:00
Leonardo de Moura
c65537aea5 feat: Option is a Monad again 
TODO: remove `OptionM` after update stage0

see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
 2022-05-04 15:27:42 -07:00
Leonardo de Moura
04d3c6feeb fix: auto implicit behavior on constructors 2022-05-04 15:04:49 -07:00
Leonardo de Moura
a1af8074c9 feat: improve discriminant refinement procedure 2022-05-04 14:46:43 -07:00
Leonardo de Moura
16ed5a3213 fix: erase_irrelevant.cpp 
It addresses issue reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/'unreachable'.20code.20was.20reached.20by.20termination.20check/near/281159704
 2022-05-04 08:06:59 -07:00
Leonardo de Moura
94b5a9b460 feat: improve split tactic 2022-05-03 17:46:50 -07:00
Gabriel Ebner
88e26b75b0 fix: actually abort with LEAN_ABORT_ON_PANIC 
The previous null-pointer dereference was UB and therefore optimized
away.
 2022-05-03 09:42:45 -07:00
Sebastian Ullrich
f6e74c677e doc: metaprogramming-arith: deduplicate 2022-05-03 18:38:36 +02:00