Skip to content
Snippets Groups Projects
Commit e6d11e79 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Argument scopes of `iProto_le`.

parent 9524aefb
No related branches found
No related tags found
No related merge requests found
Pipeline #21233 passed
Hide whitespace changes
Inline Side-by-side
theories/channel/proto_channel.v
+ 1
− 0
View file @ e6d11e79
...@@ -212,6 +212,7 @@ Local Instance iProto_le_aux_contractive {Σ} : Contractive (@iProto_le_aux Σ). ...@@ -212,6 +212,7 @@ Local Instance iProto_le_aux_contractive {Σ} : Contractive (@iProto_le_aux Σ).
Proof. solve_contractive. Qed. Proof. solve_contractive. Qed.
Definition iProto_le {Σ} (p1 p2 : iProto Σ) : iPropO Σ := Definition iProto_le {Σ} (p1 p2 : iProto Σ) : iPropO Σ :=
fixpoint iProto_le_aux p1 p2. fixpoint iProto_le_aux p1 p2.
Arguments iProto_le {_} _%proto _%proto.
Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ := Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
match vs with match vs with
......
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