Skip to content

Verify Make_indexed_subcontext.Make_set

Guillaume Claret requested to merge guillaume-claret@indexed_subcontext_make_set_eq into master

We attempt to check that the functor Make_indexed_subcontext.Make_set is actually equivalent to Make_data_set_storage.

As a result: I failed. Actually, these two are different (the path is not made in the same order 馃槥). I added in this MR some lemma which should help show that unpack and pack, used a lot in the indexed raw context, are inverses.

Edited by Guillaume Claret

Merge request reports