Skip to content
Snippets Groups Projects
Commit 22e1e914 authored by Ralf Jung's avatar Ralf Jung
Browse files

remark on a coq <-> paper difference

parent 5f230a8e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
program_logic/weakestpre.v
+ 1
− 0
View file @ 22e1e914
...@@ -57,6 +57,7 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux. ...@@ -57,6 +57,7 @@ Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
Arguments wp {_ _} _ _ _. Arguments wp {_ _} _ _ _.
Instance: Params (@wp) 4. Instance: Params (@wp) 4.
(* TODO: On paper, 'wp' is turned into a keyword. *)
Notation "#> e @ E {{ Φ } }" := (wp E e Φ) Notation "#> e @ E {{ Φ } }" := (wp E e Φ)
(at level 20, e, Φ at level 200, (at level 20, e, Φ at level 200,
format "#> e @ E {{ Φ } }") : uPred_scope. format "#> e @ E {{ Φ } }") : uPred_scope.
......
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