Beautiful, thanks, Ralf
I tried to do it, hope it worked
Dan Frumin (fd3555d0) at 24 Jul 08:38
Add local update lemmas for discrete_fun
and unit
.
... and 14 more commits
Oops, my bad. Should be fixed now
Dan Frumin (0f143d0a) at 23 Jul 11:45
fix parameter
i made the changes that were discussed here
Dan Frumin (bf77e703) at 22 Jul 19:51
simpler proof of discrete_fun_local_update
... and 11 more commits
Dan Frumin (fb5f3271) at 14 Jun 08:06
Apply 1 suggestion(s) to 1 file(s)
Dan Frumin (1023ccf7) at 13 Jun 10:23
Fix a proof for an older version
Some lemmas for the local update that we wrote with @amintimany
Dan Frumin (19e1199c) at 13 Jun 09:26
Add local update lemmas for discrete_fun
and unit
.
... and 4512 more commits
Dan Frumin (f48c5941) at 23 May 15:32
subeffects
Dan Frumin (0970b238) at 19 May 11:21
cleanup
Dan Frumin (840393c4) at 18 May 12:58
more generic effect reification
Dan Frumin (f4db42b3) at 17 May 09:27
logical relation based on WP
Dan Frumin (1996eda9) at 16 May 13:49
pairs
Dan Frumin (b6d20b66) at 16 May 13:46
adequate logical relation
Dan Frumin (462e7712) at 15 May 08:35
allow failure in reification
Dan Frumin (35c608b9) at 15 May 06:27
cleanup
Dan Frumin (cc093620) at 13 May 11:13
clean up, working on reductions generic in effects