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

perf(library/meta/rb_map): mark rb_map.mk as inline

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-03 16:11:55 -07:00
parent 09255e9a4c
commit 650a08945c
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/meta/rb_map.lean
View file

@ -18,7 +18,7 @@ meta_constant min {key : Type} {data : Type} : rb_map key data → op
meta_constant max {key : Type} {data : Type} : rb_map key data → option data
meta_constant fold {key : Type} {data : Type} {A :Type} : rb_map key data → A → (key → data → A → A) → A
meta_definition mk (key : Type) [has_cmp key] (data : Type) : rb_map key data :=
inline meta_definition mk (key : Type) [has_cmp key] (data : Type) : rb_map key data :=
mk_core data has_cmp.cmp
open list
@ -32,7 +32,7 @@ meta_definition nat_map (data : Type) := rb_map nat data
namespace nat_map
export rb_map (hiding mk)
meta_definition mk (data : Type) : nat_map data :=
inline meta_definition mk (data : Type) : nat_map data :=
rb_map.mk nat data
end nat_map
@ -40,6 +40,6 @@ meta_definition name_map (data : Type) := rb_map name data
namespace name_map
export rb_map (hiding mk)
meta_definition mk (data : Type) : name_map data :=
inline meta_definition mk (data : Type) : name_map data :=
rb_map.mk name data
end name_map