From 40d612eca0398d81b2df5ecb88c00c1178046ad4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Nov 2013 11:38:45 -0800 Subject: [PATCH] feat(library/tactic): add repeat1 and determ tacticals Signed-off-by: Leonardo de Moura --- src/library/tactic/tactic.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 8e497b64f..6c15592af 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -173,6 +173,10 @@ tactic par(tactic const & t1, tactic const & t2, unsigned check_ms = 1); \brief Return a tactic that keeps applying \c t until it fails. */ tactic repeat(tactic const & t); +/** + \brief Similar to \c repeat, but applies \c t at least once. +*/ +inline tactic repeat1(tactic const & t) { return then(t, repeat(t)); } /** \brief Similar to \c repeat, but execute \c t at most \c k times. @@ -186,6 +190,10 @@ tactic repeat_at_most(tactic const & t, unsigned k); k elements from the sequence produced by \c t. */ tactic take(tactic const & t, unsigned k); +/** + \brief Syntax sugar for take(t, 1) +*/ +inline tactic determ(tactic const & t) { return take(t, 1); } /** \brief Return a tactic that forces \c t to produce all the elements in the resultant sequence.