Skip to content

Repr: define data-encoding case validity case-by-case

Guillaume Claret requested to merge guillaume-claret@independent-data-encoding-cases into master

This does two things:

  • optimization of the proofs on data-encodings on unions by using a boolean formula to check that all the titles and tags are different
  • add a definition of validity for cases which can be expressed case by case.

However I do not achieve to express an implies lemma similar to Data_encoding.Valid.implies on Data_encoding.Valid.Case.t, due to too many dependent types. We could add that as an axiom though.

Edited by Guillaume Claret

Merge request reports