Skip to content

Commit 6a7cf61

Browse files
fix: accidental LaTeX notation (#219)
1 parent 00bb847 commit 6a7cf61

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Manual/Language/RecursiveDefs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ tag := "recursive-definitions"
2121
%%%
2222

2323
Allowing arbitrary recursive function definitions would make Lean's logic inconsistent.
24-
General recursion makes it possible to write circular proofs: "{tech}[proposition] $P$ is true because proposition $P$ is true".
24+
General recursion makes it possible to write circular proofs: "{tech}[proposition] $`P` is true because proposition $`P` is true".
2525
Outside of proofs, an infinite loop could be assigned the type {name}`Empty`, which can be used with {keywordOf Lean.Parser.Term.nomatch}`nomatch` or {name Empty.rec}`Empty.rec` to prove any theorem.
2626

2727
Banning recursive function definitions outright would render Lean far less useful: {tech}[inductive types] are key to defining both predicates and data, and they have a recursive structure.

0 commit comments

Comments
 (0)