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

fix(util/kvmap): adjust to Lean definition

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-24 20:46:40 +01:00
parent 6ea5f5196e
commit 082b217928
1 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/util/kvmap.h
View file

@ -10,13 +10,14 @@ Author: Leonardo de Moura
#include "util/name.h"
namespace lean {
enum class data_value_kind { String, Nat, Bool, Name };
enum class data_value_kind { String, Bool, Name, Nat /*, Int*/ };
/*
inductive data_value
| of_string (v : string)
| of_nat (v : nat)
| of_bool (v : bool)
| of_name (v : name)
inductive DataValue
| ofString (v : String)
| ofBool (v : Bool)
| ofName (v : Name)
| ofNat (v : Nat)
| ofInt (v : Int)
*/
class data_value : public object_ref {
data_value(b_obj_arg o, bool b):object_ref(o, b) {}