From e49a81bb563fd2d5b961a02b36b4a66a7a24f2cc Mon Sep 17 00:00:00 2001 From: Timo Date: Mon, 27 Jun 2022 17:09:41 -0400 Subject: [PATCH] doc: fix typo --- doc/examples/interp.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/examples/interp.lean b/doc/examples/interp.lean index f7326fc22b..c87c27ef92 100644 --- a/doc/examples/interp.lean +++ b/doc/examples/interp.lean @@ -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. -/