Skip to content

Draft: use SProp for well-formedness condition in Pmap and gmap

Tej Chajed requested to merge tchajed/stdpp:sprop-gmap into master

Proof of concept for #85. I'm not sure the reduction behavior is actually what we want, but I was able to get a lookup on a concrete map to reduce using only simpl (ordinarily you can get this to work with vm_compute, which breaks the opacity of proofs).

Merge request reports