leanprover / tutorial

Lean Tutorials
https://leanprover.github.io/tutorial
Apache License 2.0
44 stars 46 forks source link

Expand 7.6 #201

Open fpvandoorn opened 8 years ago

fpvandoorn commented 8 years ago

Add how dependent pattern matching works for anonymous have expressions and show expressions (the inductive definition is called this).