add a comment about the axiom-free destruct principle for lh

WasmCert · Dec 7, 2023 · 0156dfe · 0156dfe
1 parent 1e9c76f
commit 0156dfe
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/properties.v b/theories/properties.v
@@ -1593,6 +1593,8 @@ Ltac decide_eq_arg x y :=
   let Hcontra := fresh "Hcontra" in
   destruct (x == y) eqn:Heq; move/eqP in Heq; subst; last by right; move => Hcontra; injection Hcontra.
 
+(* Destruct principle for a (lh n).
+   Usage: either direct application, or `destruct ... using lh_case.` *)
 Definition lh_case: forall n (P: lholed n -> Type),
     (forall (H: 0 = n) vs es, P (lholed_cast (LH_base vs es) H)) ->
     (forall n' (H: S n' = n) vs k es (lh: lholed n') es', P (lholed_cast (LH_rec vs k es lh es') H)) ->