Skip to content

Commit

Permalink
feat(tactic/interactive): add fconstructor (#1467)
Browse files Browse the repository at this point in the history
  • Loading branch information
fpvandoorn authored and mergify[bot] committed Sep 21, 2019
1 parent 708a28c commit 9c89fa5
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions src/tactic/interactive.lean
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,9 @@ namespace tactic
namespace interactive
open interactive interactive.types expr

/-- Similar to `constructor`, but does not reorder goals. -/
meta def fconstructor : tactic unit := concat_tags tactic.fconstructor

/-- `try_for n { tac }` executes `tac` for `n` ticks, otherwise uses `sorry` to close the goal.
Never fails. Useful for debugging. -/
meta def try_for (max : parse parser.pexpr) (tac : itactic) : tactic unit :=
Expand Down

0 comments on commit 9c89fa5

Please sign in to comment.