翻訳開始

Author: s-taiga

Manual/Language/RecursiveDefs/Structural/CourseOfValuesExample.lean

@@ -12,7 +12,10 @@ import Manual.Meta
 open Verso.Genre Manual
 open Lean.Elab.Tactic.GuardMsgs.WhitespaceMode
 
+/-
 #doc (Manual) "Recursion Example (for inclusion elsewhere)" =>
+-/
+#doc (Manual) "再帰の例（Recursion Example (for inclusion elsewhere)）" =>
 
 
 :::example "Course-of-Values Tables"