Leonardo de Moura
e197021946
feat: add helper functions for creating metavariables
2019-11-21 08:10:12 -08:00
Leonardo de Moura
f2bb86f45c
refactor: use an auxiliary environment extension to implement the mutual recursion between whnf, isDefEq and inferType
...
@Kha @dselsam I was experiencing an insane code explosion with the
previous approach. There were too many definitions marked with
`@[specialize]`. `Meta.c` was reaching 0.5 million lines of code.
We would need a more sophisticated code specializer cache to handle
this kind of code. The new approach is much simpler. I don't see any
major disadvantages.
2019-11-20 16:03:45 -08:00
Leonardo de Moura
771fcdf006
feat: add isDefEqQuick
2019-11-20 10:27:38 -08:00
Leonardo de Moura
87e109aeba
feat: add isDefEqDelta
2019-11-19 17:11:20 -08:00
Leonardo de Moura
201d8a97d2
feat: add Check.lean
2019-11-19 07:09:21 -08:00
Leonardo de Moura
a3ccbe66cf
refactor: Expr fully implemented in Lean
...
No hidden fields.
2019-11-16 12:10:49 -08:00
Leonardo de Moura
c341486e28
refactor: avoid Expr constructors
...
Using `mk*` functions instead.
Reason: preparing to remove `src/kernel/expr.cpp` hack.
2019-11-14 16:32:45 -08:00
Leonardo de Moura
1f7c27672b
feat: add processAssignment
2019-11-14 12:14:46 -08:00
Leonardo de Moura
238c2b3d17
chore: add helper method
2019-11-14 09:52:41 -08:00
Leonardo de Moura
92316dff89
chore: remove unnecessary inline
2019-11-13 14:28:56 -08:00
Leonardo de Moura
fd3e038a36
feat: add isDefEqBinding
2019-11-12 16:11:25 -08:00
Leonardo de Moura
476ce17779
feat: add isDefEqArgs
2019-11-12 14:47:10 -08:00
Leonardo de Moura
8508647738
chore: remove WHNF cache
...
Remark: tried a few Lean3 stdlib and mathlib files without WHNF cache,
and did not observe any significant impact.
2019-11-12 10:07:55 -08:00
Leonardo de Moura
e12b129014
chore: add usingDefault
2019-11-12 09:46:53 -08:00
Leonardo de Moura
54868f2622
chore: SubsingletonParamInfo is not used in MetaM
2019-11-11 15:44:47 -08:00
Leonardo de Moura
320b2c9961
fix: use getConstNoEx for implementing smart unfolding
2019-11-11 11:30:22 -08:00
Leonardo de Moura
0358511121
chore: add helper
2019-11-11 11:30:22 -08:00
Leonardo de Moura
b771ec7328
feat: add basic HasToString Meta.Exception instance
2019-11-11 11:30:22 -08:00
Leonardo de Moura
269ae853b8
feat: add FunInfo
2019-11-10 18:26:57 -08:00
Leonardo de Moura
fd3786b585
chore: simplify FunInfo cache
2019-11-10 17:27:33 -08:00
Leonardo de Moura
25fed41446
feat: add forallBoundedTelescope
2019-11-10 17:12:13 -08:00
Leonardo de Moura
8653082133
fix: must take BinderInfo into account in the elaborator
...
This is not needed in the `TacticM` monad.
So, we should check if this is a bottleneck and the future.
2019-11-10 16:51:30 -08:00
Leonardo de Moura
82f521119c
feat: add isPropAux and caches for FunInfo module, rename byUnfoldingReducibleOnly => usingTransparency,
2019-11-10 16:49:07 -08:00
Leonardo de Moura
a21a024172
feat: add Meta/DefEq.lean
2019-11-10 08:55:26 -08:00
Leonardo de Moura
41fccd976b
refactor: add Lean.Meta directory for MetaM monad
2019-11-10 08:04:00 -08:00
