Make `Decidable` a subtype of `Bool` - #2038

Closed

gebner wants to merge 7 commits into

leanprover:masterfrom

gebner:decsubtype

Commits on Jan 24, 2023

fix: csimp: visit minors of casesOn in let-values
gebner
committed
db15dd4
chore: update stage0
gebner
committed
4527ca4
refactor: Bool.asProp
gebner
committed
238884b
chore: update stage0
gebner
committed
8b21496

Commits on Jan 28, 2023

chore: remove special casing for decidable in the compiler
gebner
committed
5fae78b
chore: update stage0
gebner
committed
cd0a7a1
refactor: make `Decidable` a subtype of `Bool`
gebner
committed
6cdf707