Skip to content

WIP: No SELF in lambda

Tom Jack requested to merge tomjack/mi-cho-coq:self_in_lambda into self_in_origination

This is based on !24 (closed) but takes it a bit further... perhaps too far? I'm not really saying this is the way to go. I was just experimenting.

Many of the contracts_coq are currently broken. I think it is maybe related to the simplify_instruction tactic, but I did not understand the problem yet.

Compared to !24 (closed), this forbids SELF in lambda, and eliminates the "alien" terms resulting from the (non-parametric) quantification over the self type. These do not seem like big problems. I just had this solution in my head from past attempts to precisely formalize "the Michelson type system".

Edited by Tom Jack

Merge request reports