2017-07-16から1日間の記事一覧
RustBeltの examples/get_x.v をいじってみた。 From iris.proofmode Require Import tactics. From lrust.typing Require Import typing. Set Default Proof Using "Type". Section get_x. Context `{typeG Σ}. Definition get_x : val := funrec: <> ["p"]…