Leonardo de Moura
50a43da17c
doc(tmp/fresh_name): plan for fixing mk_fresh_name
...
@kha If you have time, could you please take a look and send feedback.
I may be forgetting other problems and issues related with `mk_fresh_name`.
2018-02-01 16:19:25 -08:00
Leonardo de Moura
7f80bf60d1
feat(library/init/data): start rbtree module
2017-11-15 16:17:39 -08:00
Leonardo de Moura
3a216785ba
feat(tmp/rbtree_no_index): cleanup interface
2017-11-14 17:22:24 -08:00
Leonardo de Moura
6e4ef51f26
feat(library/tmp/rbtree_no_index): unbundled rbtree experiment
2017-11-14 12:31:53 -08:00
Leonardo de Moura
db4c9838d1
test(tmp/rbtree_no_index): rbtree without indexed families
2017-11-09 19:42:53 -08:00
Leonardo de Moura
2c3e99d538
chore(tmp): save rbtree experiment
2017-11-08 16:23:12 -08:00
Leonardo de Moura
4fbb65d9f1
feat(frontends/lean,library/equations_compiler): store tactics for generating well founded relation and decreasing proofs
2017-05-23 15:00:29 -07:00
Leonardo de Moura
729e798d6f
feat(frontends/lean/definition_cmds): copy equational lemmas to top level definition
2017-05-22 14:51:06 -07:00
Leonardo de Moura
9fb7e5c931
feat(library/equations_compiler): generate equational lemmas for auxiliary _main definitions
2017-05-21 15:21:28 -07:00
Leonardo de Moura
ce71b4c5c2
feat(frontends/lean/definition_cmds): define top-level mutual definitions
...
We still need the equational lemmas.
2017-05-21 10:26:43 -07:00
Leonardo de Moura
4e496b78d5
feat(library/equations_compiler): unpack auxiliary definition
...
We still need to unpack auxiliary lemmas, and propagate information in
the frontend.
2017-05-20 20:34:18 -07:00
Leonardo de Moura
fa863496da
feat(library/equations_compiler): prove equational lemmas for auxiliary definition
2017-05-20 16:38:32 -07:00
Leonardo de Moura
08560acf07
fix(library/equations_compiler): bugs in wf_rec
2017-05-20 13:26:49 -07:00
Leonardo de Moura
789d4e148f
feat(library/equations_compiler): add pack_mutual
...
This step packs a collection of mutually recursive functions into a
single one. We use `psum` to combine the different domains, and
`psum.cases_on` to combine the codomains.
2017-05-18 15:29:51 -07:00
Leonardo de Moura
737136e8fd
feat(library/equations_compiler/wf_rec): apply well_founded.fix
2017-05-17 16:44:53 -07:00
Leonardo de Moura
ab1a92ac3b
feat(tmp/micro_lenses): experiment with van Laarhoven-style lens
2017-03-11 11:35:02 -08:00
Leonardo de Moura
300f6b2344
chore(tmp/micro_lenses): update
2017-03-10 18:42:15 -08:00
Leonardo de Moura
b6f6126075
feat(frontends/lean/pp): add attribute [pp_using_anonymous_constructor] for marking structures we should use the anonymous constructor notation when pretty printing instances
2017-03-09 15:17:18 -08:00
Leonardo de Moura
bc01593639
chore(tmp/micro_lenses): better set for lenses.compose
2017-03-07 11:58:11 -08:00
Leonardo de Moura
cf2db32cf3
feat(tmp/micro_lenses): better definition that supports destructive updates
2017-03-07 11:18:31 -08:00
Leonardo de Moura
09c70a7e03
chore(tmp/micro_lenses): experiment for RFC
2017-03-07 09:44:10 -08:00
Leonardo de Moura
552a185e6a
feat(frontends/lean): 'let' in 'do' blocks
2017-02-24 09:10:36 -08:00
Leonardo de Moura
321105099f
feat(library/type_context): add compilation flag for disabling type inference cache
2017-02-21 20:17:25 -08:00
Leonardo de Moura
09819cb159
feat(library/type_context): add compilation flag for disabling type class resolution flag
2017-02-21 20:04:43 -08:00
Leonardo de Moura
296d4b0f09
refactor(library/tactic, library/init/meta): simplify_config => simp_config
2017-02-19 13:10:36 -08:00
Leonardo de Moura
0d22410e2e
feat(library/tactic): add zeta option, refactor simplify config option, allow users to change simplify_config in interactive mode
2017-02-19 12:11:22 -08:00
Leonardo de Moura
2928273a1e
feat(tmp/mini_crush): add experiments
2017-02-18 22:52:50 -08:00
Leonardo de Moura
a36e20f0cd
feat(tmp/mini_crush): update
2017-02-17 19:56:14 -08:00
Leonardo de Moura
aabc15823c
feat(tmp/mini_crush): add destruct_best
2017-02-16 20:50:35 -08:00
Leonardo de Moura
305838bece
refactor(library/debugger): move debugger to tools
2016-12-17 10:50:13 -08:00
Leonardo de Moura
47cd475052
feat(library): add debugger
2016-11-16 14:53:13 -08:00
Leonardo de Moura
a94368375c
feat(cli_debugger): add 'print' commands
2016-11-16 14:24:24 -08:00
Leonardo de Moura
aebe1f4946
doc(library/init/meta/vm): document VM introspection API
2016-11-16 13:05:08 -08:00
Leonardo de Moura
91c8ff746f
feat(cli_debugger): add commands for traversing stack frames
2016-11-16 12:37:18 -08:00
Leonardo de Moura
b8e904094c
feat(cli_debugger): add breakpoints
2016-11-16 10:05:36 -08:00
Leonardo de Moura
a24dbe0150
feat(cli_debugger): add breakpoint validation
2016-11-16 09:09:54 -08:00
Leonardo de Moura
cefc344ada
feat(tmp/cli_debugger): start basic CLI debugger in Lean
2016-11-15 18:42:51 -08:00
Leonardo de Moura
05013fb61d
feat(library/equations_compiler): add elim_match skeleton
2016-08-17 21:38:23 -07:00
Leonardo de Moura
c6678f3f61
chore(tmp): add wf compilation example
2016-08-12 15:34:56 -07:00
