Commit a3867545 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent 30d997f5
Pipeline #16816 failed with stage
in 15 minutes and 35 seconds
......@@ -91,8 +91,8 @@ Section lr.
(val_equiv_pre ve ty2 vh2 vc2))%I
| Lolli ty1 ty2 =>
( x (eh1: heap_lang.expr) pfh y (ec1: chan_lang.expr) pfc,
bi_pure (vh = @heap_lang.RecV BAnon x%bind eh1 pfh)
bi_pure (vc = @chan_lang.RecV BAnon y%bind ec1 pfc)
bi_pure (vh = @heap_lang.RecV BAnon x%binder eh1 pfh)
bi_pure (vc = @chan_lang.RecV BAnon y%binder ec1 pfc)
( vh1 vc1, (val_equiv_pre ve ty1 vh1 vc1
- expr_rel_lift (lift2 (val_equiv_pre ve ty2))
(App vh vh1) (chan_lang.App vc vc1))))%I
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment