Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
3f076fc836
perf: missing annotations and helper instances
2022-10-14 08:42:50 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Gabriel Ebner
3a9152f007
chore: improve defeq traces
2022-08-15 08:55:25 -07:00
Leonardo de Moura
52f3a3ff2c
refactor: move mkArrow to CoreM
2022-08-10 20:21:42 -07:00
Leonardo de Moura
18ccc01cf1
feat: add inferType for LCNF
2022-08-09 17:33:24 -07:00
Leonardo de Moura
0156b59ef1
chore: enforce naming convention
2022-08-01 09:58:11 -07:00
Patrick Massot
435017231d
doc: add some docstrings and docstrings details
2022-07-29 10:30:43 -07:00
Leonardo de Moura
6db01d8e48
perf: simpler isDefEq caching
...
We don't try to reuse the cache contents between different `isDefEq`
calls. Thus, we can cache more results and ignore whether the state of
the metavariable context affects them or not.
Closes #1102
2022-07-27 19:35:45 -07:00
Leonardo de Moura
c210781af8
refactor: add doc strings, cleanup, and dotted notation friendly API
...
See #1346
2022-07-27 16:01:15 -07:00
Leonardo de Moura
642b30ab47
feat: add withInstImplicitAsImplict
2022-07-26 12:35:30 -07:00
Leonardo de Moura
3896244c55
chore: cleanup
2022-07-25 22:39:56 -07:00
Leonardo de Moura
90fb110cc9
refactor: improve FVarId method discoverability
...
See issue #1346
2022-07-25 22:18:58 -07:00
Leonardo de Moura
8335a82aed
refactor: improve MVarId method discoverability
...
See issue #1346
2022-07-24 21:36:33 -07:00
Leonardo de Moura
a62949c49b
refactor: add type LevelMVarId (and abbreviation LMarId)
...
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.
cc @bollu
2022-07-24 17:21:45 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Mario Carneiro
f36f94a0e3
fix: malformed/misaligned markdown code fences (part 2)
2022-07-22 13:03:02 +02:00
Leonardo de Moura
da71dd3d77
chore: docstring
2022-07-18 22:16:32 -04:00
Leonardo de Moura
3fd2250799
feat: add higherOrderOutParam to ParamInfo
...
Helper info for #1299
2022-07-11 18:52:01 -07:00
Leonardo de Moura
709f22c8e4
feat: add field dependsOnHigherOrderOutParam to ParamInfo
...
See issue #1299
2022-07-11 17:49:49 -07:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Gabriel Ebner
3176943750
refactor: use computed fields for Level
2022-07-11 14:19:41 -07:00
Leonardo de Moura
55ad7beb8d
feat: add coercion placeholder for applications that return an output parameter of a local instance
2022-07-06 15:42:39 -07:00
Leonardo de Moura
2446c64a99
chore: cleanup
2022-07-04 07:15:04 -07:00
Leonardo de Moura
88fc0b2503
fix: isAssigned-like functions should set usedAssignment
2022-07-04 06:20:37 -07:00
Leonardo de Moura
6b2d2ffac6
fix: preserve usedAssignment flag when replacing MetavarContext
2022-07-04 05:49:54 -07:00
Leonardo de Moura
a1413b8fa1
feat: cache failures at isDefEq
...
We can compile Lean with these changes, but 3 tests are still broken.
This cache is used to address a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout.20with.20structures/near/288180087
2022-07-03 21:52:01 -07:00
Leonardo de Moura
aae657571f
doc: docstrings for src/Lean/Meta/Basic.lean
2022-07-03 15:32:15 -07:00
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Leonardo de Moura
e9e75af834
doc: Lean/Meta/Basic.lean
...
Add some docstrings
2022-06-30 13:32:19 -07:00
E.W.Ayers
cc9293af09
doc: isDefEq explain mvar levels
2022-06-24 15:24:52 -07:00
Leonardo de Moura
f6d1e48cb8
fix: constant => opaque issues
2022-06-14 17:19:54 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
e997cd94c6
chore: style
2022-05-31 06:04:48 -07:00
Leonardo de Moura
6af1da450e
feat: disable only eta for classes during TC resolution
...
closes #1123
2022-04-26 08:20:39 -07:00
Leonardo de Moura
7d99f6f555
perf: isClassQuick? was incorrectly producing undef
...
Then `isClassExpensive?` was being invoked too often. In some
benchmarks the performance hit was substantial. For example,
in the new test `state8.lean`. The runtime on my machine went from 2s
to 0.76s.
2022-04-09 10:38:49 -07:00
Leonardo de Moura
6e02514eee
chore: style
2022-04-09 10:27:31 -07:00
Leonardo de Moura
cd0d7e676f
chore: rename renameMVar => setMVarUserName
2022-04-07 13:50:58 -07:00
Leonardo de Moura
46ce3013d0
feat: cleanup local context before elaborating match alternatives RHS
2022-03-29 18:52:07 -07:00
E.W.Ayers
534aa88188
doc: MetaM
2022-03-24 16:57:42 -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
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
0bd9de1cb9
perf: add InstantiateLevelCaches for types and values at CoreM
2022-03-15 17:42:38 -07:00
Leonardo de Moura
ca253c43e1
refactor: pattern elaboration
...
We don't use the following hack anymore:
- /- HACK: `fvarId` is not in the scope of `mvarId`
- If this generates problems in the future, we should update the metavariable declarations. -/
- assignExprMVar mvarId (mkFVar fvarId)
This hack was corrupting the `InfoTree`.
2022-03-09 18:19:14 -08:00
Leonardo de Moura
50ae170bcc
feat: allow mkLambdaFVars and mkForallFVars to abstract unassigned metavars too
2022-03-09 11:27:58 -08:00
Leonardo de Moura
1263cea6af
feat: add support for unassigned metavariables at dependsOn
2022-03-09 11:27:58 -08:00
