max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(tactic/exact_tactic): exact_core that takes transparency

Browse source
This commit is contained in:
Daniel Selsam 2016-12-10 20:22:18 -08:00 • committed by Leonardo de Moura
parent b2c1ea6fdb
commit 317989bf9e
2 changed files with 13 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/init/meta/tactic.lean
View file

@ -286,7 +286,7 @@ meta constant mk_mapp_core : transparency → name → list (option expr) → t
Otherwise, try to find a local constant that has type of the form (t = t') or (t' = t).
The tactic fails if the given expression is not a local constant. -/
meta constant subst : expr → tactic unit
meta constant exact : expr → tactic unit
meta constant exact_core : transparency → expr → tactic unit
/- Elaborate the given quoted expression with respect to the current main goal.
If the boolean argument is tt, then metavariables are tolerated and
become new goals. -/
@ -491,6 +491,12 @@ get_local n >>= infer_type
meta def trace_result : tactic unit :=
format_result >>= trace
meta def exact : expr → tactic unit :=
exact_core semireducible
meta def rexact : expr → tactic unit :=
exact_core reducible
/- (find_same_type t es) tries to find in es an expression with type definitionally equal to t -/
meta def find_same_type : expr → list expr → tactic expr
| e [] := failed

11
src/library/tactic/exact_tactic.cpp
View file

@ -9,11 +9,12 @@ Author: Leonardo de Moura
#include "library/tactic/app_builder_tactics.h"
namespace lean {
vm_obj exact(expr const & e, tactic_state const & s) {
vm_obj exact_core(transparency_mode const & m, expr const & e, tactic_state const & s) {
try {
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
type_context ctx = mk_type_context_for(s);
type_context ctx = mk_type_context_for(s, m);
expr e_type = ctx.infer(e);
if (!ctx.is_def_eq(g->get_type(), e_type)) {
auto thunk = [=]() {
@ -34,12 +35,12 @@ vm_obj exact(expr const & e, tactic_state const & s) {
}
}
vm_obj tactic_exact(vm_obj const & e, vm_obj const & s) {
return exact(to_expr(e), to_tactic_state(s));
vm_obj tactic_exact_core(vm_obj const & m, vm_obj const & e, vm_obj const & s) {
return exact_core(to_transparency_mode(m), to_expr(e), to_tactic_state(s));
}
void initialize_exact_tactic() {
DECLARE_VM_BUILTIN(name({"tactic", "exact"}), tactic_exact);
DECLARE_VM_BUILTIN(name({"tactic", "exact_core"}), tactic_exact_core);
}
void finalize_exact_tactic() {