diff --git a/src/util/list_fn.cpp b/src/util/list_fn.cpp new file mode 100644 index 000000000..e5ecc9b2a --- /dev/null +++ b/src/util/list_fn.cpp @@ -0,0 +1,19 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/list.h" + +namespace lean { +list mk_list_range(unsigned from, unsigned to) { + list r; + unsigned i = to; + while (i > from) { + i--; + r = cons(i, r); + } + return r; +} +}