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

chore: mark inferInstance and inferInstanceAs as [inline]

Browse source 
New code generator does not inline simple declarations not tagged with
`[inline]` yet. We need this change to simpilify testing
This commit is contained in:
Leonardo de Moura 2022-08-17 19:08:51 -07:00
parent ff53e9cc56
commit 8985a15f96
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

@ -83,7 +83,7 @@ example : foo.default = (default, default) :=
rfl
```
-/
@[reducible] def inferInstance {α : Sort u} [i : α] : α := i
abbrev inferInstance {α : Sort u} [i : α] : α := i
set_option checkBinderAnnotations false in
/-- `inferInstanceAs α` synthesizes a value of any target type by typeclass
@ -97,7 +97,7 @@ does.) Example:
#check inferInstanceAs (Inhabited Nat) -- Inhabited Nat
```
-/
@[reducible] def inferInstanceAs (α : Sort u) [i : α] : α := i
abbrev inferInstanceAs (α : Sort u) [i : α] : α := i
set_option bootstrap.inductiveCheckResultingUniverse false in
/--