Type erasure

Stream: lean4

[ohhaimark]

Does lean implement some form of type erasure? If so, does a pattern match that is the identity on erased terms become the identity function?

[James Gallicchio]

yes! the compiler throws out almost all type information at runtime -- take a look at the manual for how types get converted to their C representation

[James Gallicchio]

and if a pattern match only has one live branch (for instance, if all other branches end in by contradiction), then the match is turned into straight-line control flow