Skip to content

Commit c0f6733

Browse files
committed
fix tests
1 parent c7abbe3 commit c0f6733

File tree

2 files changed

+4
-4
lines changed

2 files changed

+4
-4
lines changed

tests/lean/run/symbolFrequency.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,4 @@ open Lean PremiseSelection
77
#guard_msgs in
88
run_meta do
99
let f ← symbolFrequency `Nat
10-
logInfo m!"{decide (10000 < f)}"
10+
logInfo m!"{decide (5000 < f)}"

tests/lean/run/symbolFrequency_foldRelevantConsts.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,19 @@ open Lean PremiseSelection
99
#guard_msgs in
1010
run_meta do
1111
let ci ← getConstInfo `List.append_assoc
12-
let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
12+
let consts ← ci.type.foldRelevantConsts (init := #[]) (fun n ns => return ns.push n)
1313
logInfo m!"{consts}"
1414

1515
/-- info: [List, Ne, HAppend.hAppend, List.nil, Eq, List.head] -/
1616
#guard_msgs in
1717
run_meta do
1818
let ci ← getConstInfo `List.head_append_right
19-
let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
19+
let consts ← ci.type.foldRelevantConsts (init := #[]) (fun n ns => return ns.push n)
2020
logInfo m!"{consts}"
2121

2222
/-- info: [Array, Nat, LT.lt, Array.size, HAdd.hAdd, OfNat.ofNat, Array.swap, Not] -/
2323
#guard_msgs in
2424
run_meta do
2525
let ci ← getConstInfo `Array.eraseIdx.induct
26-
let consts ← foldRelevantConsts ci.type (init := #[]) (fun n ns => return ns.push n)
26+
let consts ← ci.type.foldRelevantConsts (init := #[]) (fun n ns => return ns.push n)
2727
logInfo m!"{consts}"

0 commit comments

Comments
 (0)