Turn stuff like iRes Definitions instead of Notations.

With Set Printing All, these notations make me loose overview entirely.

Turn stuff like iRes Definitions instead of Notations.
With Set Printing All, these notations make me loose overview entirely.
31f0ec05 · Robbert Krebbers · 3fdd636a · 31f0ec05
Commit 31f0ec05 authored Feb 23, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 5 additions and 5 deletions

program_logic/model.v program_logic/model.v +5 -5

No files found.
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -31,11 +31,11 @@ End iProp.

 (* Solution *)
 Definition iPreProp (Λ : language) (Σ : iFunctor) : cofeT := iProp.result Λ Σ.
-Notation iRes Λ Σ := (res Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iResRA Λ Σ := (resRA Λ Σ (laterC (iPreProp Λ Σ))).
-Notation iWld Λ Σ := (mapRA positive (agreeRA (laterC (iPreProp Λ Σ)))).
-Notation iPst Λ := (exclRA (istateC Λ)).
-Notation iGst Λ Σ := (ifunctor_car Σ (laterC (iPreProp Λ Σ))).
+Definition iRes Λ Σ := res Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iResRA Λ Σ := resRA Λ Σ (laterC (iPreProp Λ Σ)).
+Definition iWld Λ Σ := mapRA positive (agreeRA (laterC (iPreProp Λ Σ))).
+Definition iPst Λ := exclRA (istateC Λ).
+Definition iGst Λ Σ := ifunctor_car Σ (laterC (iPreProp Λ Σ)).
 Definition iProp (Λ : language) (Σ : iFunctor) : cofeT := uPredC (iResRA Λ Σ).
 Definition iProp_unfold {Λ Σ} : iProp Λ Σ -n> iPreProp Λ Σ := solution_fold _.
 Definition iProp_fold {Λ Σ} : iPreProp Λ Σ -n> iProp Λ Σ := solution_unfold _.