From 2012dcfc7f9c6a3dfa050d8297fd07f716d49bac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 9 Feb 2019 09:20:07 -0800 Subject: [PATCH] chore(util/string_ref): add `string_refs` alias --- src/util/string_ref.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/string_ref.h b/src/util/string_ref.h index 33c7b25267..53659a719c 100644 --- a/src/util/string_ref.h +++ b/src/util/string_ref.h @@ -7,6 +7,7 @@ Author: Leonardo de Moura #pragma once #include #include "util/object_ref.h" +#include "util/list_ref.h" namespace lean { /* Wrapper for Lean string objects */ class string_ref : public object_ref { @@ -31,4 +32,5 @@ public: friend bool operator==(string_ref const & s1, char const * s2) { return string_eq(s1.raw(), s2); } friend bool operator!=(string_ref const & s1, char const * s2) { return !(s1 == s2); } }; +typedef list_ref string_refs; };