Commit 0010b710 authored by Robbert Krebbers's avatar Robbert Krebbers

Params for `iProto_le`.

parent c7701c44
Pipeline #25606 passed with stage
in 19 minutes and 41 seconds
......@@ -216,6 +216,7 @@ Proof. solve_contractive. Qed.
Definition iProto_le `{invG Σ} (p1 p2 : iProto Σ) : iProp Σ :=
fixpoint iProto_le_aux p1 p2.
Arguments iProto_le {_ _} _%proto _%proto.
Instance: Params (@iProto_le) 2 := {}.
Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
match vs with
......
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