Leonardo de Moura
cfcbb6e9dc
fix: typo
2019-11-11 11:30:22 -08:00
Leonardo de Moura
27567d85e3
fix: typo
2019-11-11 11:30:22 -08:00
Leonardo de Moura
95eb3d525f
fix: typo
2019-11-11 11:30:22 -08:00
Leonardo de Moura
b4cc85e92d
fix: typo
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
d138d068dd
chore: fix typo
2019-11-11 11:30:22 -08:00
Leonardo de Moura
93d3ab3f8c
chore: add aux fixpoint
2019-11-11 11:30:22 -08:00
Leonardo de Moura
bd1b1af781
chore: simplify signature
2019-11-10 18:33:31 -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
20e8086fea
feat: add Hashable (Option a) instance
2019-11-10 17:25:32 -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
Daniel Selsam
bff5e4ed37
feat: solves mvars in reverse order during tabled tc
2019-11-09 21:15:34 -08:00
Leonardo de Moura
1dd8770b3a
feat: forallTelescope and forallTelescopeReducing
2019-11-09 21:10:12 -08:00
Leonardo de Moura
c62355e26b
feat: inferType for let expressions
2019-11-09 20:44:27 -08:00
Leonardo de Moura
cff9e4192d
feat: add inferLambdaType
2019-11-09 20:33:29 -08:00
Leonardo de Moura
c44517c876
chore: fix tests
2019-11-09 20:32:28 -08:00
Leonardo de Moura
00131b14f6
feat: add MetaM.mkForall and MetaM.mkLambda
2019-11-09 20:23:17 -08:00
Leonardo de Moura
981cd44eaa
feat: add lambdaTelescope
2019-11-09 20:20:18 -08:00
Daniel Selsam
f574cdf5e0
feat: fresh contexts for each new subgoal
2019-11-09 15:51:23 -08:00
Daniel Selsam
9ce13e93c9
feat: allow metas in intermediate tc answers
2019-11-09 15:49:39 -08:00
Daniel Selsam
0bab51b66e
feat: solve typeclass subgoals in reverse order
...
Some instance arguments may still need to be reversed.
2019-11-09 15:47:50 -08:00
Sebastian Ullrich
dac6f273b5
feat: simplistic linter framework
2019-11-09 15:43:37 -08:00
Leonardo de Moura
c33a1f977f
feat: ensure isClass unfolds only reducible constants
2019-11-09 14:02:11 -08:00
Leonardo de Moura
d72b22572d
feat: update vector of local instances
2019-11-09 13:49:27 -08:00
Leonardo de Moura
adcb9091ef
fix: avoid redundant let-decls
2019-11-09 12:32:31 -08:00
Leonardo de Moura
1e065d495b
feat: expose hasLooseBVar
2019-11-09 12:29:50 -08:00
Leonardo de Moura
3592f6d34d
chore: withCacheScope => savingCache
2019-11-09 12:17:46 -08:00
Leonardo de Moura
5d3b1f09d2
chore: add TODO
2019-11-09 12:07:09 -08:00
Leonardo de Moura
1eccb19401
feat: add inferForallType
2019-11-09 12:00:45 -08:00
Leonardo de Moura
d54880b6d1
feat: helper functions for debugging, handling metavars, creating telescopes, extract universe level from types, checking whether type is a class, and declaring locals
2019-11-09 11:37:32 -08:00
Leonardo de Moura
d10e08236f
feat: add finally
2019-11-09 07:28:12 -08:00
Leonardo de Moura
e5b77d4de8
feat: combine InferType and TypeUtil into Meta
2019-11-08 16:20:11 -08:00
Leonardo de Moura
d9fb5acb22
chore: use same approach we use for HashMap
2019-11-08 08:28:31 -08:00
Leonardo de Moura
90178cf923
chore: add helper functions
2019-11-08 08:28:31 -08:00
Leonardo de Moura
5c39ea7faa
feat: add InferProjType
2019-11-08 08:28:31 -08:00
Leonardo de Moura
a2cdf4494d
chore: add helper
2019-11-08 08:28:31 -08:00
Leonardo de Moura
2009068a53
feat: add getLooseBVarRange
2019-11-08 08:28:31 -08:00
Leonardo de Moura
f1847ef75f
feat: add inferType helper functions
2019-11-08 08:28:31 -08:00
Leonardo de Moura
54ce57fe26
feat: add instantiateRevRange
2019-11-08 08:28:31 -08:00
Leonardo de Moura
583923492c
chore: naming conventions
2019-11-07 10:40:26 -08:00
Leonardo de Moura
322f18f0c9
chore: WHNFUtil => WHNF
2019-11-07 10:25:58 -08:00
Daniel Selsam
f272f42c1f
fix: (throwaway) context was ignoring const levels
2019-11-07 10:21:24 -08:00
Leonardo de Moura
91e87a0cd4
feat: add reference implementation for whnf
2019-11-07 10:20:15 -08:00
Leonardo de Moura
e020cd2ea0
refactor: parametrize over getConst : Name -> m (Option (ConstantInfo)) instead of env : Environment
...
Motivation: when instatiating these templates, we can make definitions
opaque by returning `none` at `getConst`.
2019-11-07 10:20:15 -08:00
Leonardo de Moura
a087aea871
chore: remove special support for user-facing projection functions
...
We now have kernel projections, and user-facing projection functions
are defined using them. So, we don't need special support anymore for
them. They are just regular functions in Lean4.
2019-11-07 10:20:15 -08:00
