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

chore: change inferInstance and inferInstanceAs types

Browse source
This commit is contained in:
Leonardo de Moura 2021-02-21 08:36:03 -08:00
parent ae48feeb07
commit b1faed895a
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Prelude.lean
View file

@ -18,8 +18,8 @@ abbrev Function.comp {α : Sort u} {β : Sort v} {δ : Sort w} (f : β → δ) (
abbrev Function.const {α : Sort u} (β : Sort v) (a : α) : β → α :=
fun x => a
@[reducible] def inferInstance {α : Type u} [i : α] : α := i
@[reducible] def inferInstanceAs (α : Type u) [i : α] : α := i
@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i
set_option bootstrap.inductiveCheckResultingUniverse false in
inductive PUnit : Sort u where