search

leanprover / theorem_proving_in_lean4

Theorem Proving in Lean 4
https://leanprover.github.io/theorem_proving_in_lean4/
Apache License 2.0
164 stars 92 forks source link

fix(doc): update the examples of inferred types #10

Closed SteveUlin closed 2 years ago

SteveUlin commented 3 years ago

The current examples of interfered types in lambda expressions contain types. Remove these types to avoid confusion.