Checker "tenet" on test "corner-cases/eta-struct-major-and"
Checker: tenet · Version: 0.11.3 · 📄 Declaration · 🔗 Source
Test: corner-cases/eta-struct-major-and · Expected: 🤷 either · Size: 9.4 KB · Lines: 175 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration · 🔗 Source
Result: ✋ rejected · exit code 1 · wall time: 126 ms · instructions: 817.8 M · max rss memory: 44.9 MB · run 2026-10-24 16:42:18 UTC
stdout:
FAIL thm andMajorEta (0.01s)
declaration type mismatch for 'andMajorEta'
expected: ∀ (P : Prop), ∀ (Q : Prop), ∀ (A : Type), ∀ (f : P → Q → A), ∀ (x : And P Q), Eq.{1} A (And.rec.{1} P Q (fun (x.«_@».Test.3893811644._hygCtx._hyg.27 : And P Q) => A) f (And.intro P Q (And.left P Q x) (And.right P Q x))) (And.rec.{1} P Q (fun (x.«_@».Test.3893811644._hygCtx._hyg.27 : And P Q) => A) f x)
inferred: ∀ (P : Prop), ∀ (Q : Prop), ∀ (A : Type), ∀ (f : P → Q → A), ∀ (x : And P Q), Eq.{1} A (And.rec.{1} P Q (fun (x.«_@».Test.3893811644._hygCtx._hyg.27 : And P Q) => A) f x) (And.rec.{1} P Q (fun (x.«_@».Test.3893811644._hygCtx._hyg.27 : And P Q) => A) f x)
FAILED: 4 checked, 1 failed, 0 skipped, 9 constants, 0.1s, 4 jobs