[OCaml] High Intensity Training Online
docs trim interface docs to intent and invariant
Interface docs stated design choices by defending them against roads not taken ("not merely bookkeeping", "must be free to diverge", "never a quantity to compute or configure"). Per the steering, a header should say what the module is for and which invariant it upholds — not re-argue the shape. Cut the defensive asides; kept the doctrinal grounding and the edge-case notes.
Changed files
lib/core/entry.mli
@@ -54,9 +54,8 @@
54
54
val is_finished : t -> bool
55
55
56
56
val duration : t -> Recovery.duration option
57
Removed:
(** [Some] once finished. HD1 treats a shortening duration on the same workout
58
Removed:
as rising intensity, so this is a progress signal and not mere bookkeeping.
59
Removed:
*)
57
Added:
(** [Some] once finished. HD1 reads a shortening duration on the same workout as
58
Added:
rising intensity, so it is a progress signal. *)
60
59
61
60
val stimuli : t -> Stimulus.t list
62
61
(** In the order performed. *)
lib/core/progression.mli
@@ -6,8 +6,7 @@
6
6
Its central asymmetry is Mentzer's: when progress halts, the answer is never
7
7
more work. HD1 is explicit that the urge to raise volume and frequency on a
8
8
stall "must be kept in check and avoided at all costs", so no remedy here
9
Removed:
can add either. That is structural — there is only one remedy, and it
10
Removed:
subtracts. *)
9
Added:
can add either — there is one remedy, and it subtracts. *)
11
10
12
11
(** {1 Progress} *)
13
12
@@ -55,9 +54,8 @@
55
54
in cardiorespiratory failure before the muscle does. *)
56
55
57
56
val load_increase : current:Units.Weight.t -> Units.Weight.t * Units.Weight.t
58
Removed:
(** The 10-20% window to move into. A window rather than a figure: HD1 says "or
59
Removed:
any amount necessary" to be forced back into the rep range, and what a bar
60
Removed:
can actually be loaded to is not a training principle. *)
57
Added:
(** The 10-20% window to move into. A window, not a figure: HD1 says "or any
58
Added:
amount necessary" to be forced back into the rep range. *)
61
59
62
60
type load_verdict =
63
61
| Hold (** The load still places failure inside the window. *)
lib/core/recovery.mli
@@ -1,11 +1,11 @@
1
1
(** Recovery: the elapsed time between two workouts, judged against a
2
2
recommended window, and the permission to train that follows from it.
3
3
4
Removed:
HD1 treats recovery as a precondition of growth rather than a suggestion —
5
Removed:
training before the body has replenished its reserves is the primary error,
6
Removed:
and its effects are systemic, not local to the muscles worked. So readiness
7
Removed:
is not merely reported: starting a workout requires a {!clearance}, which is
8
Removed:
either earned by resting or taken deliberately and on the record. *)
4
Added:
HD1 treats recovery as a precondition of growth: training before the body
5
Added:
has replenished its reserves is the primary error, and its effects are
6
Added:
systemic, not local to the muscles worked. So starting a workout requires a
7
Added:
{!clearance}, either earned by resting or taken deliberately and on the
8
Added:
record. *)
9
9
10
10
type timestamp = private int
11
11
lib/core/stimulus.mli
@@ -1,15 +1,10 @@
1
1
(** One stimulus: a single drive to muscular failure, and the record of what it
2
2
took.
3
3
4
Removed:
This is the unit of work. HD1 prescribes one set per exercise, so there is
5
Removed:
no set count to record and no "set group" wrapping anything — how the drive
6
Removed:
was delivered is a property of the stimulus itself.
4
Added:
The unit of work. HD1 prescribes one set per exercise, so there is no set
5
Added:
count. Reaching failure is not recorded because it is not optional — a
6
Added:
movement here always went to failure. *)
7
7
8
Removed:
Reaching failure is not recorded because it is not optional: a movement here
9
Removed:
always went to failure, which is what distinguishes a stimulus from mere
10
Removed:
exercise. What varies is the load, the reps it happened to yield, and
11
Removed:
whether anything carried the effort past failure. *)
12
Removed:
13
8
(** A means of continuing past positive failure. HD1 treats these as occasional:
14
9
used on every exercise they lead straight to overtraining, and forced reps
15
10
and negatives both need a spotter. *)
@@ -59,8 +54,7 @@
59
54
end
60
55
61
56
(** How the stimulus was delivered — the performed counterpart of
62
Removed:
{!Prescription.delivery}. Deliberately a separate type: the two sides carry
63
Removed:
different data and must be free to diverge. *)
57
Added:
{!Prescription.delivery}. *)
64
58
type delivery =
65
59
| Single of Movement.t
66
60
| Pre_exhaust of { isolation : Movement.t; compound : Movement.t }
lib/core/workout_prescription.mli
@@ -2,8 +2,8 @@
2
2
sequence of prescribed stimuli.
3
3
4
4
Each prescription is exactly one drive to failure, so the workout's volume
5
Removed:
is its length — HD1's "least amount required" is structural here, never a
6
Removed:
quantity to compute or configure. Static: no history, no targets. *)
5
Added:
is its length — HD1's "least amount required" is structural here. Static: no
6
Added:
history, no targets. *)
7
7
8
8
type t
9
9
type id = private string