feat(util): add (functional) name_map
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
dcacf6fbca
commit
e155708dda
1 changed files with 12 additions and 0 deletions
12
src/util/name_map.h
Normal file
12
src/util/name_map.h
Normal file
|
@ -0,0 +1,12 @@
|
||||||
|
/*
|
||||||
|
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||||
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
|
Author: Leonardo de Moura
|
||||||
|
*/
|
||||||
|
#pragma once
|
||||||
|
#include "util/rb_map.h"
|
||||||
|
#include "util/name.h"
|
||||||
|
namespace lean {
|
||||||
|
template<typename T> using name_map = rb_map<name, T, name_quick_cmp>;
|
||||||
|
}
|
Loading…
Reference in a new issue