max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(util/string_ref): add string_refs alias

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-09 09:20:07 -08:00
parent e8758a1707
commit 2012dcfc7f
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/string_ref.h
View file

@ -7,6 +7,7 @@ Author: Leonardo de Moura
#pragma once
#include <string>
#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_ref> string_refs;
};