From 63b9060ce91d45472a694479f66279039b4deec9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Mar 2022 16:23:06 -0700 Subject: [PATCH] chore: fix comments --- tests/lean/run/nativeReflBackdoor.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/lean/run/nativeReflBackdoor.lean b/tests/lean/run/nativeReflBackdoor.lean index a3d64a2d1f..08ad3f7da4 100644 --- a/tests/lean/run/nativeReflBackdoor.lean +++ b/tests/lean/run/nativeReflBackdoor.lean @@ -1,7 +1,7 @@ -- /- -This example demonstratea that when we are using `nativeDecide`, +This example demonstratea that when we are using `native_decide`, we are also trusting the correctness of `implementedBy` annotations, foreign functions (i.e., `[extern]` annotations), etc. -/ @@ -18,7 +18,7 @@ def f (b : Bool) := b theorem fConst (b : Bool) : f b = false := match b with | true => - /- The following `nativeDecide` is going to use `g` to evaluate `f` + /- The following `native_decide` is going to use `g` to evaluate `f` because of the `implementedBy` directive. -/ have : (f true) = false := by native_decide this