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

4324 commits

Author SHA1 Message Date
Wojciech Nawrocki
96770b4d83 refactor: remove some code duplication 2022-03-26 06:26:41 -07:00
Wojciech Nawrocki
9223bf3640 feat: environment extension for RPC procedures 2022-03-26 06:26:41 -07:00
Leonardo de Moura
a2e467eb32 fix: mkEqnTypes 
stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.

This commit fixes the last issue exposed by #1074

fixes #1074
 2022-03-25 19:13:21 -07:00
Leonardo de Moura
3a310fb122 fix: the eta for structures implementation in the elaborator was different from the implementation in the kernel 
This issue was exposed by issue #1074
 2022-03-25 18:24:15 -07:00
Leonardo de Moura
e53435979f fix: remove hacky addAutoBoundImplicitsOld 2022-03-25 09:23:43 -07:00
Leonardo de Moura
6631d92d7b fix: addAutoBoundImplicitsOld occurrences at MutualDef.lean and Structure.lean 
This commit also fixes non-termination at `collectUnassignedMVars`
 2022-03-25 09:07:59 -07:00
Leonardo de Moura
e48cc8901e fix: add new addAutoBoundImplicits that avoids the hack at addAutoBoundImplicitsOld 2022-03-25 08:40:57 -07:00
Leonardo de Moura
519b780164 doc: document InfoTree issue 2022-03-25 07:12:07 -07:00
Leonardo de Moura
370e9c421f fix: bug at deriving Hashable 2022-03-24 18:46:10 -07:00
E.W.Ayers
534aa88188 doc: MetaM 2022-03-24 16:57:42 -07:00
E.W.Ayers
1e69639fd2 doc: clarify mkLocalDecl 2022-03-24 14:59:46 -07:00
E.W.Ayers
6f5fc72c06 doc: Docstrings for LocalContext.lean 2022-03-24 14:59:46 -07:00
E.W.Ayers
24ebd78071 doc: Expr.lean 2022-03-24 14:52:09 -07:00
Wojciech Nawrocki
8f83c7ab32 feat: user-defined RPC handlers 2022-03-24 08:09:33 -07:00
Leonardo de Moura
fdbe893c40 fix: catch mkAppM exceptions 2022-03-23 17:35:04 -07:00
Leonardo de Moura
e0aa9fb290 chore: fix typo 2022-03-23 07:39:46 -07:00
Leonardo de Moura
2f67140603 fix: incorrect uses of getMVarType' 2022-03-22 14:11:29 -07:00
Leonardo de Moura
6007147d71 fix: allow universes to be postponed further 
closes #1058
 2022-03-22 13:57:58 -07:00
Leonardo de Moura
f3b181b972 chore: comment withoutPostponingUniverseConstraints 2022-03-22 13:57:58 -07:00
Mario Carneiro
c29da66c5a
fix: annotate binders in intro for hover / go to def 2022-03-22 12:10:51 +00:00
Sebastian Ullrich
c4d3c74837 feat: accept multiple patterns after matches 2022-03-21 17:59:02 +01:00
Sebastian Ullrich
faedfbe651 fix: antiquotation splices early in bootstrapping 2022-03-21 17:44:15 +01:00
Leonardo de Moura
3d9e587862 fix: check type mismatch at dependent pattern matching compiler 
see issue #1057
 2022-03-21 09:28:02 -07:00
Leonardo de Moura
321d6b0e67 feat: support for user-defined simp attributes in the simp tactic. 
See `RELEASES.md`

TODO: make sure `-thm` also removes `thm` from user-defined simp attributes.
 2022-03-20 18:45:57 -07:00
Leonardo de Moura
a2690d5278 feat: improve #eval command 2022-03-20 15:18:47 -07:00
Leonardo de Moura
6d926c7989 feat: macro expand match alternatives 
see #371

This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
  | S (s : String)
  | I (i : Int)

def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
  match x with
  | I a => toString a
  | S a => toString a
```
 2022-03-20 14:20:13 -07:00
Leonardo de Moura
8f4d58893f feat: update match parser 
Support for
```
def fib (x : Nat) : Nat :=
  match x with
  | 0 | 1 => 1
  | x+2   => fib (x+1) + fib x
```

TODO: expand `matchAlts`
 2022-03-20 13:22:39 -07:00
Leonardo de Moura
3862e7867b refactor: make String.Pos opaque 
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`

closes #410
 2022-03-20 10:47:13 -07:00
Jakob von Raumer
a91f92c11e feat: allow constants to be type classes 
There no reason against constants to be type classes so it is just the check in `addClass` that is needed to be modified.

Closes #1054
 2022-03-20 08:03:34 -07:00
Leonardo de Moura
1b357db3b0 fix: nasty bug at findDeclarationRangesCore? 
We must search the environment extension first, and then the builtin
table. Otherwise, the builtin declarations do not change when we
modify the files.

closes #1021
 2022-03-19 16:53:22 -07:00
Leonardo de Moura
ed7c8904a9 fix: propagate local and scope modifiers at elab_rules 
closes #1039
 2022-03-19 16:08:06 -07:00
Leonardo de Moura
82cd5c8eef chore: cleanup 2022-03-19 15:52:04 -07:00
E.W.Ayers
da68f629f9 style: Apply.lean 
Apply Leo's review requests.
 2022-03-19 15:51:40 -07:00
E.W.Ayers
d954706fcf feat: ApplyNewGoals config for apply 
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.

Closes #1045
 2022-03-19 15:51:40 -07:00
Leonardo de Moura
c95d5f25a3 feat: convert ites into dites in the WF module 
Motivation: the condition is often used in termination proofs.
 2022-03-19 10:11:50 -07:00
Leonardo de Moura
36d955e8cc feat: use simpler encoding for nonmutually recursive definitions 2022-03-19 09:43:18 -07:00
Leonardo de Moura
c7cdbf8ff8 feat: improve auto generated termination_by a bit 2022-03-19 09:28:19 -07:00
Leonardo de Moura
7dd38a7194 feat: add with_unfolding_all and rfl' tactics 2022-03-19 08:57:04 -07:00
Leonardo de Moura
fa74194638 fix: missing s.restore at expandTacticMacroFns 2022-03-19 08:34:54 -07:00
Leonardo de Moura
bd7827ed04 feat: dbg_trace tactic for low-level tactic debugging 2022-03-19 08:25:49 -07:00
Leonardo de Moura
a486503c62 chore: fold Nat literals at reduce 2022-03-18 17:10:46 -07:00
Leonardo de Moura
1514e39006 chore: add double ticks 2022-03-18 17:10:46 -07:00
Leonardo de Moura
42b707e250 perf: improve getMatchWithExtra 2022-03-18 17:10:46 -07:00
Leonardo de Moura
38a1675c72 fix: dicrimination tree getMatchWithExtra 
It was buggy when the input argument could be reduced `e`.

fixes #1048
 2022-03-17 16:44:38 -07:00
Leonardo de Moura
3193acecfa fix: flush the CoreM and MetaM caches at modifyEnv 
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.

We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.

I tried a few benchmarks and did not notice a significant difference.

cc @kha @gebner

fixes #1051
 2022-03-17 16:02:30 -07:00
Leonardo de Moura
719db55a9c chore: fix trace class 2022-03-17 13:22:16 -07:00
Leonardo de Moura
184b0b8e8d feat: improve "result types must be in the same universe level" error message 
The new error message makes it clear why the definition is not accepted.

See issue #1050
 2022-03-17 07:41:37 -07:00
Daniel Fabian
969eea19f0 refactor: do not use mkAppM so much 2022-03-16 17:21:20 -07:00
Daniel Fabian
cf4e873974 feat: support Sort u in ac_refl. 2022-03-16 17:21:20 -07:00
Daniel Fabian
8e0763f502 fix: binder case. 2022-03-16 17:21:20 -07:00