search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

add missing word #71

Closed holtzermann17 closed 5 years ago

holtzermann17 commented 5 years ago

First, Lean supports mutually defined inductive types. The idea is that we can define two (or more) inductive types at the same time, where each one refers to the other(s).

I think that's the correct substitution for the missing word.