This is a (very) experimental, and only partially completed shallow embedding of the proposed new typechecker for solidity into lean4.
Core solidity blocks currently do not have any custom syntax expansion, and are implemented by
simply writing the restricted subset of monadic lean code that matches the proposal. Custom syntax
for Yul is implemented and assembly {} blocks are macro expanded into monadic lean4 code.