edd5e97045
This is a hard coded extra case. It is not an instance of has_coe. Even if we change has_coe to accomodate this case, it will not be a satisfactory solution because this coercion depends on the element and not the type, and the element usually contains metavariables. We should eventually write a tactic for synthesizing coercions. |
||
|---|---|---|
| .. | ||
| anf.lean | ||
| builtin.lean | ||
| cf.lean | ||
| config.lean | ||
| default.lean | ||
| format.lean | ||
| internal.lean | ||
| ir.lean | ||
| pass.lean | ||
| procedure.lean | ||
| result.lean | ||
| util.lean | ||