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

chore: fix comments

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-30 16:23:06 -07:00
parent 3dd0c84c4d
commit 63b9060ce9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/nativeReflBackdoor.lean
View file

@ -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