diff --git a/library/init/meta/environment.lean b/library/init/meta/environment.lean index be88ffedbb..c959105a21 100644 --- a/library/init/meta/environment.lean +++ b/library/init/meta/environment.lean @@ -87,6 +87,7 @@ meta constant structure_fields : environment → name → option (list name) occurring in instances of type classes tagged with the attribute `attr_name`. Example: [algebra] -/ meta constant get_class_attribute_symbols : environment → name → name_set +meta constant fingerprint : environment → nat open expr meta constant unfold_untrusted_macros : environment → expr → expr diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index d8e52e7976..09f73711b7 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -14,6 +14,7 @@ Author: Leonardo de Moura #include "library/class.h" #include "library/projection.h" #include "library/util.h" +#include "library/fingerprint.h" #include "library/relation_manager.h" #include "library/inductive_compiler/ginductive.h" #include "library/vm/vm_nat.h" @@ -251,6 +252,10 @@ vm_obj environment_get_class_attribute_symbols(vm_obj const & env, vm_obj const return to_obj(get_class_attribute_symbols(to_env(env), to_name(n))); } +vm_obj environment_fingerprint(vm_obj const & env) { + return mk_vm_nat(mpz(get_fingerprint(to_env(env)))); +} + void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "mk_std"}), environment_mk_std); DECLARE_VM_BUILTIN(name({"environment", "trust_lvl"}), environment_trust_lvl); @@ -280,6 +285,7 @@ void initialize_vm_environment() { DECLARE_VM_BUILTIN(name({"environment", "unfold_untrusted_macros"}), environment_unfold_untrusted_macros); DECLARE_VM_BUILTIN(name({"environment", "structure_fields"}), environment_structure_fields); DECLARE_VM_BUILTIN(name({"environment", "get_class_attribute_symbols"}), environment_get_class_attribute_symbols); + DECLARE_VM_BUILTIN(name({"environment", "fingerprint"}), environment_fingerprint); } void finalize_vm_environment() {