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

4189 commits

Author SHA1 Message Date
Sebastian Ullrich
e9b8e54dcc feat: scientific parser alias for scientificLit 2022-03-08 18:54:05 +01:00
Jonathan Coates
11cce61e4d chore: Clean up LSP folding a little 
- Wait for all terms to be elaborated before showing folding regions.
   May want to change this to support partial results.
 - Use .span to extract import statements, rather than mutually
   recursive functions.
 - Some tiny other bits of cleanup
 2022-03-07 17:23:35 +01:00
Jonathan Coates
04e60cebd1 feat: LSP code folding support 
The following constructs are foldable:
 - Sections and namespaces
 - Blocks of import/open statements
 - Multi-line commands (so mostly definitions)
 - Mutual definitions
 - Module-level doc comments
 - Top-level definition doc comments

Fixes #1012
 2022-03-07 17:23:35 +01:00
Sebastian Ullrich
ff097e952f chore: link orphan file 2022-03-07 10:59:49 +01:00
Leonardo de Moura
46d1111d3d fix: typo at unfoldBothDefEq 2022-03-06 13:54:42 -08:00
Leonardo de Moura
ff0f3bfc61 fix: interaction between overloaded notation and delayed coercions 
The new test exposes this issue.
 2022-03-06 09:49:15 -08:00
Leonardo de Moura
b664a93d8e fix: a match application is stuck if one of the discriminants contain metavariables 2022-03-06 07:51:09 -08:00
Leonardo de Moura
8bcaafb28b fix: universe metavariables should not be taken into account at getKeyArgs 2022-03-06 07:50:19 -08:00
Leonardo de Moura
b105c006a5 fix: PrefixTree WellFormed type 
`β` is a parameter.
 2022-03-06 07:30:34 -08:00
Leonardo de Moura
1450a86c4d feat: include types in the "ambiguous, possible interpretations" error message 2022-03-06 07:26:31 -08:00
Leonardo de Moura
3f9c854194 feat: auto local implicit chaining 2022-03-05 17:30:15 -08:00
Leonardo de Moura
f7130d8e07 refactor: use CPS at addAutoBoundImplicits 
We want to be able to declare new local variables there.
 2022-03-05 16:24:33 -08:00
Leonardo de Moura
22731c02b0 fix: auto implicit locals in inductive families 2022-03-05 15:47:20 -08:00
Leonardo de Moura
613cf19509 fix: discrimination trees and "stuck" terms 
See comments and new test.
 2022-03-05 15:12:20 -08:00
Leonardo de Moura
d39102f865 fix: smart unfolding for reducible definitions 
When `TransparencyMode.reducible`, smart unfolding for reducible
definitions was not being used.
 2022-03-05 14:42:47 -08:00
Leonardo de Moura
9e76cd7d65 fix: toName function at elabAppFnId 
closes #1038
 2022-03-04 16:56:02 -08:00
Leonardo de Moura
a670ed1e2d fix: use withoutErrToSorry at apply 
closes #1037
 2022-03-04 14:36:10 -08:00
Leonardo de Moura
8b248e2d8c feat: elaborate for h : x in xs do ... notation 2022-03-03 19:52:26 -08:00
Leonardo de Moura
5d2420b1c9 chore: add auxiliary notation for ForIn' 2022-03-03 19:10:24 -08:00
Leonardo de Moura
92937b3aba feat: add for h : x in xs do ... notation 
The idea is to have `h : x \in xs`.
This commit just adds the parser.
 2022-03-03 18:27:40 -08:00
Leonardo de Moura
b745c4f51a fix: recursive overapplication at WF/Fix.lean 2022-03-03 18:13:34 -08:00
Leonardo de Moura
f306c9b69b fix: split tactic 
`unreachable!` assertions at `simpIfLocalDecl` and
`simpTargetLocalDecl` were reachable.
 2022-03-03 18:13:34 -08:00
Leonardo de Moura
f4e98be163 fix: use whnfD at mkNoConfusion 
The `split` tactic failed at `Array.sizeOf_lt_of_mem` because the type
in the equality is `Id Bool` when we write `true` instead of `id true`.
 2022-03-03 18:13:34 -08:00
Leonardo de Moura
137c70f055 chore: add LinearArith/Nat/Solver.lean 2022-03-03 11:13:40 -08:00
Leonardo de Moura
043d338271 feat: add getForbiddenByTrivialSizeOf 2022-03-03 11:12:32 -08:00
Leonardo de Moura
1f2618adba feat: delaborate cond using bif-then-else 2022-03-03 07:41:39 -08:00
Leonardo de Moura
1155d52702 chore: update TODO comment 2022-03-02 12:51:46 -08:00
Leonardo de Moura
093ab49b7f feat: improve generateElements a bit 2022-03-02 11:58:47 -08:00
Leonardo de Moura
52403fca83 feat: add support for guessing (very) simple WF relations 
There are a lot of TODOs, but it is already useful for simple cases.

closes #847
 2022-03-02 11:52:00 -08:00
Leonardo de Moura
99204d2226 refactor: modify elabWFRel to CPS 2022-03-02 11:52:00 -08:00
Leonardo de Moura
88a2645a5f refactor: add Lean/Meta/Tactic/LinearArith/Basic.lean 2022-03-02 11:52:00 -08:00
Leonardo de Moura
f171286e74 refactor: add src/Lean/Meta/Tactic/LinearArith/Nat 2022-03-02 11:52:00 -08:00
Sebastian Ullrich
c9713b1b69 fix: setExpectedFn 2022-03-02 16:28:53 +01:00
Leonardo de Moura
1e205d635e fix: bug at wfRecursion 
"After compilation" attributes were being applied to soon when we did
not need to generate auxiliary functions.
 2022-03-01 17:48:06 -08:00
Leonardo de Moura
140559c447 feat: sizeOf for Thunks and Unit -> a 2022-03-01 16:40:11 -08:00
Leonardo de Moura
85a1a5233b chore: workaround for compiler closed term extraction issue 2022-03-01 09:01:08 -08:00
Leonardo de Moura
5948003601 feat: add support for constant folding Nat.beq, Nat.blt, and Nat.ble 2022-03-01 09:01:08 -08:00
Leonardo de Moura
4e310ac63d feat: improve SimpTheorem preprocessor 2022-02-28 18:27:36 -08:00
Leonardo de Moura
adf3510e08 chore: increase maxHeartbeats default values 
We now increase the number of heartbeats at `expr_eq_fn`. Thus, the
old default values are too small.
 2022-02-28 15:44:08 -08:00
Leonardo de Moura
55bc048656 feat: make sure inequalities are normalized when no monomial was cancelled 2022-02-28 15:10:39 -08:00
Leonardo de Moura
e455df9c95 fix: use a def-eq aware mapping at toLinearExpr 
The new test exposes the problem fixed by this commit.
In the termination proof we have two `sizeOf xs` terms that are not
syntactically identical (only definitional equal) because the
instances are different.
 2022-02-28 13:46:36 -08:00
Leonardo de Moura
10657f5e81 feat: add trace <string> tactic 2022-02-28 11:16:42 -08:00
Leonardo de Moura
63a5cd5056 fix: trace_state messages should not be lost during backtracking 2022-02-28 11:07:41 -08:00
Leonardo de Moura
d89fa9d4c3 fix: endPos missing at trace messages 2022-02-28 10:55:45 -08:00
Sebastian Ullrich
53d313c74c chore: fix function name 2022-02-28 16:16:22 +01:00
Leonardo de Moura
c5fdd54cd8 feat: support for acyclicity at unifyEqs 
closes #1022
 2022-02-27 10:03:40 -08:00
Leonardo de Moura
89f88b1caa feat: simplify nested arith expressions 2022-02-27 09:01:52 -08:00
Leonardo de Moura
c5baf759e2 fix: we must use addAsAxiom before getFixedPrefix 
`getFixedPrefix` uses `isDefEq`, and it will fail if it needs to
retrieve the type of one of the recursive function being defined.
 2022-02-27 09:01:52 -08:00
Sebastian Ullrich
6c6f66b812 feat: propagate actual file name in file worker 
Also stop recreating the FileMap for every command, that's quadratic!
 2022-02-27 10:33:27 +01:00
Leonardo de Moura
f22b48b226 fix: display all remaining goals at fail tactic error message 2022-02-26 09:49:06 -08:00