Commit af23632c authored by Lennard Gäher's avatar Lennard Gäher
Browse files

more implicit types

parent 73e86fad
......@@ -5,7 +5,7 @@ From semantics.axiomatic Require Export hoare_lib.
Import hoare.
Implicit Types
(P Q: iProp)
(P Q R: iProp)
(φ ψ: Prop)
(e: expr)
(v: val).
......
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