fix(src/builtin/tactic): add default rule set if none is provided
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
b55aee1efd
commit
e2540b68db
1 changed files with 3 additions and 0 deletions
|
@ -19,6 +19,9 @@ tactic_macro("unfold", { macro_arg.Id }, function (env, id) return unfold_tac(id
|
||||||
|
|
||||||
tactic_macro("simp", { macro_arg.Ids },
|
tactic_macro("simp", { macro_arg.Ids },
|
||||||
function (env, ids)
|
function (env, ids)
|
||||||
|
if #ids == 0 then
|
||||||
|
ids[1] = "default"
|
||||||
|
end
|
||||||
return simp_tac(ids)
|
return simp_tac(ids)
|
||||||
end
|
end
|
||||||
)
|
)
|
||||||
|
|
Loading…
Reference in a new issue