Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • Villetaneuse/lambda-rust
  • iris/lambda-rust
  • maximedenes/LambdaRust-coq
  • msammler/lambda-rust
  • daniel.louwrink/lambda-rust
  • simonspies/lambda-rust
  • xldenis/lambda-rust
  • lgaeher/lambda-rust
  • JasonHuZS/lambda-rust
  • snyke7/lambda-rust
  • ivanbakel/lambda-rust
11 results
Show changes
Commits on Source (1)
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/typing/perm.v
View file @ 0657f6bf
...@@ -118,7 +118,7 @@ Section has_type. ...@@ -118,7 +118,7 @@ Section has_type.
WP ν @ E {{ Φ }}. WP ν @ E {{ Φ }}.
Proof. Proof.
iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type. iIntros "H◁ HΦ". setoid_rewrite has_type_value. unfold has_type.
destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". destruct (eval_expr ν) eqn:EQν; last by iDestruct "H◁" as "[]". simpl.
iMod ("HΦ" $! v with "[] H◁") as "HΦ". done. iMod ("HΦ" $! v with "[] H◁") as "HΦ". done.
iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH" iInduction ν as [| | |[] e ? [|[]| | | | | | | | | |] _| | | | | | | |] "IH"
forall (Φ v EQν); try done. forall (Φ v EQν); try done.
......