diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 19299f727b..34fa4219f2 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -55,7 +55,7 @@ public: \remark #start_iteration unblocks it. */ void block_new_info(); - /** \breif Mark the start of a new information collection cycle. + /** \brief Mark the start of a new information collection cycle. It also enables new information to be added, i.e., it will undo the effect of #block_new_info. */ diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h index 219c5d1ea0..0f840e499e 100644 --- a/src/kernel/default_converter.h +++ b/src/kernel/default_converter.h @@ -15,7 +15,7 @@ Author: Leonardo de Moura #include "kernel/expr_pair.h" namespace lean { -/** \breif Converter used in the kernel */ +/** \brief Converter used in the kernel */ class default_converter : public converter { protected: typedef std::unordered_set expr_pair_set; diff --git a/src/library/class_instance_synth.h b/src/library/class_instance_synth.h index 73e06e13b9..8611840c9e 100644 --- a/src/library/class_instance_synth.h +++ b/src/library/class_instance_synth.h @@ -41,10 +41,10 @@ optional mk_class_instance(environment const & env, io_state const & ios, name const & prefix, expr const & type, bool use_local_instances = true, unifier_config const & cfg = unifier_config()); -/** \breif Try to synthesize an inhabitant for (is_hset type) using class instance resolution */ +/** \brief Try to synthesize an inhabitant for (is_hset type) using class instance resolution */ optional mk_hset_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type); -/** \breif Try to synthesize an inhabitant for (subsingleton type in the standard library, and hprop in the HoTT library) +/** \brief Try to synthesize an inhabitant for (subsingleton type in the standard library, and hprop in the HoTT library) using class instance resolution */ optional mk_subsingleton_instance(type_checker & tc, io_state const & ios, list const & ctx, expr const & type);