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

feat(library/init/core): eagerly expanding Decidable.toBool seems to be a bad idea

Browse source 
After we erase types and proofs, `Decidable.toBool` can be replaced with
the identity function since `Decidable A` and `Bool` have the same
runtime representation. By eagerly expanding `toBool`, we introduce
unnecessary `cases` expressions.
This commit is contained in:
Leonardo de Moura 2019-03-25 15:24:51 -07:00
parent 5679a17603
commit 7db4f60e50
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/core.lean
View file

@ -846,7 +846,7 @@ Exists.rec h₂ h₁
/- Decidable -/
@[macroInline] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
@[inlineIfReduce, nospecialize] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool :=
Decidable.casesOn h (λ h₁, false) (λ h₂, true)
instance beqOfEq {α : Type u} [DecidableEq α] : HasBeq α :=

4
src/library/compiler/erase_irrelevant.cpp
View file

@ -342,6 +342,10 @@ class erase_irrelevant_fn {
return visit_quot_mk(args);
} else if (fn == get_quot_lift_name()) {
return visit_quot_lift(args);
} else if (fn == get_decidable_to_bool_name() && args.size() == 2) {
/* Decidable.toBool is the "identify" function since Decidable and Bool have
the same runtime representation. */
return args[1];
}
}
return visit_app_default(f, args);