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

doc: fix typo

Browse source
This commit is contained in:
Timo 2022-06-27 17:09:41 -04:00 • committed by Leonardo de Moura
parent 34dc2572f3
commit e49a81bb56
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/examples/interp.lean
View file

@ -38,7 +38,7 @@ We can write a function to translate `Ty` values to a Lean type
— remember that types are first class, so can be calculated just like any other value.
We mark `Ty.interp` as `[reducible]` to make sure the typeclass resolution procedure can
unfold/reduce it. For example, suppose Lean is trying to synthesize a value for the instance
`Add (Ty.interp Ty.int)`. Since `Ty.interp` is marked as `[reducible],
`Add (Ty.interp Ty.int)`. Since `Ty.interp` is marked as `[reducible]`,
the typeclass resolution procedure can reduce `Ty.interp Ty.int` to `Int`, and use
the builtin instance for `Add Int` as the solution.
-/