Skip to content

Commit d06782d

Browse files
committed
add docstring Indep
1 parent e8e6aa0 commit d06782d

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

AesopTest/Forward/SynthIndep.lean

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,21 @@ testIndep 6 50 by
7070
trivial
7171
-/
7272

73+
/--
74+
#### Independent rules.
75+
76+
This test compares the efficiency of the procedures on independent rules
77+
and hypotheses.
78+
79+
Consider a set of propositions `P := {Pᵢⱼ | 1 ≤ i ≤ nRs and 1 ≤ j ≤ nPs}` and
80+
`Q := {Qᵢ | 1 ≤ i ≤ nRs}`.
81+
We run the procedures we with the `nRs` following rules `rᵢ : Pᵢ₁ → ... → Pᵢₙₚₛ → Qᵢ`
82+
and a context containing precisely `P`.
83+
84+
- `nPs` : Number of premises in the rules.
85+
- `nRs` : Number of unique rules; they are independent but have the same number
86+
of premises.
87+
-/
7388
def runTestIndep (nPs : Nat) (nRs : Nat) : CommandElabM Nanos := do
7489
let mut nPs := Syntax.mkNatLit nPs
7590
let mut nRs := Syntax.mkNatLit nRs

0 commit comments

Comments
 (0)