Normalizing Casts and Coercions

01/28/2020
by   Robert Y. Lewis, et al.
0

This system description introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frustrating for beginning and expert users alike; the presence of coercions can cause seemingly identical expressions to fail to unify. The norm_cast tactics aim to make reasoning with such expressions as transparent as possible.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset