metaprogramming / introspection

Stream: LftCM22

[Ryan McCorvie]

@Leonardo de Moura do you think meta-programming and introspection will be used for constructing proofs themselves? Like you introspect a different proof, formally change it with meta-programming constructs, then assert that as the proof to a new proposition? (Sorry, I didn't get a chance to ask this in the session)

[Mario Carneiro]

@Ryan McCorvie This is already being done by the @[to_additive] attribute in lean 3 and lean 4