From 1637d75d3f03d9f14595a0f44d691686bd38785f Mon Sep 17 00:00:00 2001 From: Josh Levine Date: Sun, 9 Jan 2022 04:19:26 -0500 Subject: [PATCH] doc: fix trivial typo --- doc/thunk.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/thunk.md b/doc/thunk.md index d536b4f4ae..3400b7668f 100644 --- a/doc/thunk.md +++ b/doc/thunk.md @@ -54,7 +54,7 @@ def g (c : Bool) (x : Nat) : Nat := ``` In the following example, we use the macro `dbg_trace` to demonstrate that the Lean runtime caches the value computed by a `Thunk`. -We remark that the macro `dbg_trace` should be use for debugging purposes +We remark that the macro `dbg_trace` should be used for debugging purposes only. ```lean def add1 (x : Nat) : Nat :=