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

24300 commits

This branch
This branch
All branches
Author SHA1 Message Date
Sebastian Ullrich
ed55fdfd3e chore: better error message when failing to find current package 2021-03-23 12:10:26 +01:00
Leonardo de Moura
81e6181488 test: add another test 2021-03-22 21:21:14 -07:00
Leonardo de Moura
650c6df380 feat: try other variables after failure 2021-03-22 21:02:26 -07:00
Leonardo de Moura
17907a7829 fix: perform topological sort on pattern variables 2021-03-22 20:35:07 -07:00
Sebastian Ullrich
ed9c3ba525 doc: LHS precedences 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
cd4cd581be feat: make infix non-associative 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
2180898192 fix: |>. must parse its arguments 
... since we want it to have a low precedence, which now precludes it
from being used in function position
 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
bbf6c717fc feat: introduce arg precedence 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
9f6436ebfd chore: reset prefer_native 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
a798101c08 chore: update stage0 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
725c0c1911 chore: implement lhs prec 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
61229b7d2d chore: update stage0 2021-03-22 16:33:37 +01:00
Sebastian Ullrich
3d90850fdd feat: add syntax for specifying LHS precedence on trailing parsers 2021-03-22 16:33:36 +01:00
Leonardo de Moura
3749213e08 fix: missing whnf at Unify.unify 2021-03-21 22:38:46 -07:00
Leonardo de Moura
2fd0b8c663 feat: contradiction catches empty inductive types 2021-03-21 21:48:43 -07:00
Leonardo de Moura
3d6154f147 fix: contradiction 
It must ignore auxiliary declarations.
 2021-03-21 20:05:15 -07:00
Leonardo de Moura
123783d5f9 fix: some issues at cases and subst 2021-03-21 18:35:31 -07:00
Leonardo de Moura
880f1372bd feat: set pp.inaccessibleNames true when visualizing tactic state 
@Kha The default value (false) for `pp.inaccessibleNames == false` help when
visualizing error messages (see test
`hidingInaccessibleNames.lean`). We added this feature after to hide
intermediate variables created by `match_syntax`.
However, this default value confused me in tactic mode. For example,
it will hide a hypotheses `x : Fin 0` if nobody depends on it, but as
a user we want to know we have it since we can close the goal using
it. Thus, I added `withPPInaccessibleNames act`, it executes `act`
using `pp.inaccessibleNames true` if the user did not explicitly set
it. I use this combinator at `FileWorker` and when producing the
`unsolved goals` error message. In all other scenarios, I believe
hiding these inaccessible variables is a good thing.
 2021-03-21 18:21:46 -07:00
Leonardo de Moura
19b24e3e82 chore: update stage0 2021-03-20 18:53:41 -07:00
Leonardo de Moura
d9273786c7 chore: remove when and «unless» 
They are obsolete.

cc @Kha
 2021-03-20 18:52:18 -07:00
Leonardo de Moura
9a5f239513 refactor: remove Monad Option and Alternative Option 
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.

cc @Kha
 2021-03-20 18:25:25 -07:00
Leonardo de Moura
7d61a61407 chore: udpate stage0 2021-03-20 17:51:04 -07:00
Leonardo de Moura
04e3f21783 chore: add OptionM monad 
Motivation: `Option` is data, `OptionM` is control.
 2021-03-20 17:50:45 -07:00
Sebastian Ullrich
29c7db3ed2 feat: term info at many more constants 2021-03-20 08:31:06 -07:00
Sebastian Ullrich
83ecff44c6 test: make infoTree an output test 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
c0af90022e feat: term info at #print 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
c86f41a42b feat: command-level info trees 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
86072873f4 feat: server: allow more than one ContextInfo 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
62891a1b0c feat: trace.Elab.info 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
2f168e3364 feat: mkConstWithLevelParams 2021-03-20 08:28:18 -07:00
Sebastian Ullrich
d34ef570a7 chore: print unexpected internal frontend errors 2021-03-20 08:28:18 -07:00
Daniel Selsam
c0d8e09a2f fix: bug in normLtAux 2021-03-20 08:21:08 -07:00
Sebastian Ullrich
e62542ed29 feat: CoeSort Bool Prop 2021-03-20 14:52:16 +01:00
Leonardo de Moura
86a204d8a1 feat: add simp_all tactic 
cc @Kha
 2021-03-19 22:34:35 -07:00
Leonardo de Moura
d70740fef2 fix: location notation and simp 2021-03-19 19:54:22 -07:00
Leonardo de Moura
94465e8a02 feat: add helper simp methods 2021-03-19 14:11:15 -07:00
Leonardo de Moura
03e3a1cc6b chore: remove hack 
It produces weird error messages in some examples, and it will be
obsolete after the new precedence feature.
 2021-03-19 11:09:18 -07:00
Sebastian Ullrich
54405c4543 fix: automatically wrap many/sepBy items in null nodes where necessary 2021-03-19 15:15:55 +01:00
Leonardo de Moura
da8e5150c9 feat: add getNondepPropHyps 2021-03-18 14:25:50 -07:00
Leonardo de Moura
dd8ead186f feat: allow caller to set lemma id 2021-03-18 14:25:16 -07:00
Leonardo de Moura
f73615c3d2 fix: nontermination 2021-03-18 14:23:03 -07:00
Leonardo de Moura
b7c82d40a2 chore: fix isHole code 2021-03-18 07:39:13 -07:00
Leonardo de Moura
9daed5e91d chore: add checkLinebreakBefore 2021-03-18 06:43:03 -07:00
Leonardo de Moura
1af02dcaca feat: allow users to mark definitions with [simp] 
cc @JasonGross @Kha
 2021-03-17 19:11:55 -07:00
Leonardo de Moura
7213b02c7e chore: update stage0 2021-03-17 18:53:11 -07:00
Leonardo de Moura
3208faa192 feat: add set of declarations to unfold at SimpLemmas 2021-03-17 18:52:23 -07:00
Leonardo de Moura
205b42a397 feat: proper syntax for configuring simp 2021-03-17 16:37:04 -07:00
Leonardo de Moura
f7028b36a4 chore: update stage0 2021-03-17 16:22:00 -07:00
Leonardo de Moura
f25f0edda4 chore: prepare to update simp notation 2021-03-17 16:21:10 -07:00
Leonardo de Moura
5eda786f6e feat: use False.elim when simplifying local declarations that rewrite to False 2021-03-17 15:30:54 -07:00