From f7dd85a9357ef9f9fe8533cbaf9bdb884cda4dd4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 8 Jun 2015 16:54:55 -0700 Subject: [PATCH] chore(*): fix 'breif' typos --- src/frontends/lean/info_manager.h | 2 +- src/kernel/default_converter.h | 2 +- src/library/class_instance_synth.h | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) 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);