Commit 720536fa authored by Ralf Jung's avatar Ralf Jung

document base_logic.upred

parent e7266df5
From iris.algebra Require Export cmra. From iris.algebra Require Export cmra.
Set Default Proof Using "Type*". Set Default Proof Using "Type*".
(** The basic definition of the uPred type, its metric and functor laws.
You probably do not want to import this file. Instead, import
base_logic.base_logic; that will also give you all the primitive
and many derived laws for the logic. *)
Record uPred (M : ucmraT) : Type := IProp { Record uPred (M : ucmraT) : Type := IProp {
uPred_holds :> nat M Prop; uPred_holds :> nat M Prop;
uPred_mono n x1 x2 : uPred_holds n x1 x1 {n} x2 uPred_holds n x2; uPred_mono n x1 x2 : uPred_holds n x1 x1 {n} x2 uPred_holds n x2;
......
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