Open sm4sa opened 1 year ago
Having no prior experience with lean, I am unfamiliar with its syntax. I would recommend including a link/recommendation to basic lean syntax. For example, some links that might be helpful include for inductive type declaration: https://leanprover.github.io/reference/declarations.html#inductive-types https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html#:~:text=It%20is%20also%20known%20as,elements%20beyond%20those%20they%20construct.
Having no prior experience with lean, I am unfamiliar with its syntax. I would recommend including a link/recommendation to basic lean syntax. For example, some links that might be helpful include for inductive type declaration: https://leanprover.github.io/reference/declarations.html#inductive-types https://leanprover.github.io/theorem_proving_in_lean4/inductive_types.html#:~:text=It%20is%20also%20known%20as,elements%20beyond%20those%20they%20construct.