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

fix: typos in specialize.cpp (#2702)

Browse source
This commit is contained in:
SADIK KUZU 2023-10-17 03:58:10 +03:00 • committed by GitHub
parent 4441662490
commit e0802d2dea
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/library/compiler/specialize.cpp generated
View file

@ -175,7 +175,7 @@ environment update_spec_info(environment const & env, comp_decls const & ds) {
name_set S;
spec_info_buffer d_infos;
name_generator ngen;
/* Initialzie d_infos and S */
/* Initialize d_infos and S */
for (comp_decl const & d : ds) {
S.insert(d.fst());
d_infos.push_back(pair<name, buffer<spec_arg_kind>>());
@ -546,7 +546,7 @@ class specialize_fn {
/* Recall that `m_ctx.m_vars` contains all variables (lambda and let) the specialization
depends on, and `m_ctx.m_params` contains the ones that should be lambda abstracted. */
m_ctx.m_vars.push_back(x);
/* Thus, a variable occuring outside of a binder is only lambda abstracted if it is not
/* Thus, a variable occurring outside of a binder is only lambda abstracted if it is not
a let-variable. */
if (!v) m_ctx.m_params.push_back(x);
}
@ -959,7 +959,7 @@ class specialize_fn {
types, and it will fail to infer the type of `n`-applications if we do not have
an entry in the environment.
Remark: we mark the axiom as `meta` to make sure it does not polute the environment
Remark: we mark the axiom as `meta` to make sure it does not pollute the environment
regular definitions.
We also considered the following cleaner solution: modify `csimp` to use a custom