Merge pull request #11 from sinianluoye/issue/7

fix no auxiliary matching function issue

Author: sinianluoye

Manual/Elaboration.lean

@@ -424,7 +424,7 @@ A definition that still includes recursion, but has otherwise been elaborated to
 To see auxiliary pattern matching functions in Lean's output, set the option {option}`pp.match` to {lean}`false`.
 -/
 
-这种转化分为两步：首先，在项繁释期间，将用到的模式匹配替换为实现特定区分的 {deftech key:="auxiliary"}_辅助匹配函数_。
+这种转化分为两步：首先，在项繁释期间，将用到的模式匹配替换为实现特定区分的 {deftech key:="auxiliary matching function"}_辅助匹配函数_。
 这些辅助函数自身由归递器定义，且不必真的用到归递器的递归功能。{margin}[它们会用到 `casesOn`，具体参见{ref "recursor-elaboration-helpers"}[归递器与繁释帮助章节]。]
 项繁释器最终返回的核心项中，模式匹配已被这种特殊函数替代，但仍有递归出现。尚包含递归但其它方面已繁释为核心语言的定义称为 {deftech key := "pre-definition"}[前定义]。
 若需在 Lean 输出里看到辅助模式匹配函数，可设置 {option}`pp.match` 为 {lean}`false`。