Skip to content

Don't axiomatize operations

Raphaël Cauderlier requested to merge rafoo@unaxiomatize_operations into dev

This defines an algebraic type to represent operations. This allows pattern-matching on the operations emitted by a contract which is required to integrate Mi-Cho-Coq with contract interaction frameworks such as ConCert. This is also related to https://gitlab.com/nomadic-labs/coquille/-/issues/5.

Merge request reports