diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 768f688b8cbed02c6220c1d026d390977e51622e..a73b968c4a6327722009c3274626a7acb2cb8d6e 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -32,6 +32,10 @@ Inductive dfrac :=
   | DfracDiscarded : dfrac
   | DfracBoth : Qp → dfrac.
 
+(* This notation is intended to be used as a component in other notations that
+   include discardable fractions. The notation provides shorthands for the
+   constructors and the commonly used full fraction. For and example
+   demonstrating how this can be used see the notation in [gen_heap.v]. *)
 Declare Custom Entry dfrac.
 Notation "{ dq }" := (dq) (in custom dfrac at level 1, dq constr).
 Notation "â–¡" := DfracDiscarded (in custom dfrac).