lean4-htt/src/library/blast
2015-09-30 13:31:42 -07:00
..
blast.cpp refactor(library/blast): rename lref to href (hypothesis reference) 2015-09-29 12:13:20 -07:00
blast.h feat(library/blast): convert goal into blast state 2015-09-25 14:44:00 -07:00
blast_context.h feat(library/blast): add helper functions to access blast tactic thread local state/context 2015-09-29 10:04:11 -07:00
blast_exception.h feat(library/blast): add basic blast_exception 2015-09-29 09:02:58 -07:00
blast_tactic.cpp feat(library/blast): add basic blast_exception 2015-09-29 09:02:58 -07:00
blast_tactic.h feat(library/blast): parse blast tactic and invoke stub 2015-09-25 12:45:16 -07:00
branch.cpp refactor(library/blast): change how we mark fixed/frozen hypothesis 2015-09-29 14:08:14 -07:00
branch.h refactor(library/blast): change how we mark fixed/frozen hypothesis 2015-09-29 14:08:14 -07:00
CMakeLists.txt refactor(library/blast): revise how goal meta-vars are compiled into blast mrefs 2015-09-28 16:40:19 -07:00
expr.cpp feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more 2015-09-30 13:31:42 -07:00
expr.h feat(kernel/level,library/blast/expr): add universe level hash consing support in the kernel, simplify blast/expr even more 2015-09-30 13:31:42 -07:00
hypothesis.h refactor(library/blast): change how we mark fixed/frozen hypothesis 2015-09-29 14:08:14 -07:00
init_module.cpp feat(library/blast): finish goal -> state translation 2015-09-28 17:39:30 -07:00
init_module.h feat(library/blast): parse blast tactic and invoke stub 2015-09-25 12:45:16 -07:00
state.cpp refactor(library/blast): change how we mark fixed/frozen hypothesis 2015-09-29 14:08:14 -07:00
state.h refactor(library/blast): change how we mark fixed/frozen hypothesis 2015-09-29 14:08:14 -07:00
union_find.h feat(library/blast): add union-find datastructure 2015-05-11 16:19:51 -07:00