You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: Manual/Language/RecursiveDefs.lean
+1-1Lines changed: 1 addition & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -21,7 +21,7 @@ tag := "recursive-definitions"
21
21
%%%
22
22
23
23
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".
25
25
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.
26
26
27
27
Banning recursive function definitions outright would render Lean far less useful: {tech}[inductivetypes]arekeytodefiningbothpredicatesanddata,andtheyhavearecursivestructure.
0 commit comments