leanprover / reference-manual

Apache License 2.0
25 stars 3 forks source link

Coercions #146

Open david-christiansen opened 1 week ago

david-christiansen commented 1 week ago

What question should the reference manual answer?

What are coercions? When are they inserted? What is the difference between head, tail, function, dependent, and ordinary coercions? When should I define each?