Open subfish-zhou opened 1 week ago
认领任务:在对应issue下评论然后在群里@subfish-zhou,我会invite you to be collaborator !!注意!!请使用最新mathlib4 文件在MIL文件夹下,文本翻译格式遵循 https://github.com/avigad/mathematics_in_lean_source/?tab=readme-ov-file#markup
范例:https://github.com/Lean-zh/math-in-lean-zh/blob/master/MIL/C01_Introduction/S01_Getting_Started.lean 翻译规范(术语表,标点符号格式):https://github.com/Agda-zh/PLFA-zh/issues/1 (本项目无法保留原文)
认领任务:在对应issue下评论然后在群里@subfish-zhou,我会invite you to be collaborator !!注意!!请使用最新mathlib4 文件在MIL文件夹下,文本翻译格式遵循 https://github.com/avigad/mathematics_in_lean_source/?tab=readme-ov-file#markup
范例:https://github.com/Lean-zh/math-in-lean-zh/blob/master/MIL/C01_Introduction/S01_Getting_Started.lean 翻译规范(术语表,标点符号格式):https://github.com/Agda-zh/PLFA-zh/issues/1 (本项目无法保留原文)