(module eq_user_adt_smoke
  (data Point
    (doc "Two-Int-field record. The milestone-defining north-star: an LLM author writes `instance Eq Point` and calls `(app eq p1 p2)` end-to-end through class-dispatch.")
    (ctor Point (con Int) (con Int)))
  (instance
    (class prelude.Eq)
    (type (con Point))
    (doc "Eq Point by structural comparison of the two Int fields. The nested `(app eq a1 a2)` calls dispatch to prelude.Eq.eq's Int instance.")
    (method eq
      (body (lam
        (params (typed p1 (con Point)) (typed p2 (con Point)))
        (ret (con Bool))
        (body
          (match p1
            (case (pat-ctor Point a1 b1)
              (match p2
                (case (pat-ctor Point a2 b2)
                  (if (app eq a1 a2) (app eq b1 b2) false))))))))))
  (fn main
    (type (fn-type (params) (ret (own (con Unit))) (effects IO)))
    (params)
    (body
      (let p1 (term-ctor Point Point 1 2)
        (let p2 (term-ctor Point Point 1 2)
          (let p3 (term-ctor Point Point 1 3)
            (seq (seq (app print (app eq (lit-unit) (lit-unit))) (do io/print_str "\n"))
              (seq (seq (app print (app eq p1 p2)) (do io/print_str "\n"))
                (seq (app print (app eq p1 p3)) (do io/print_str "\n"))))))))))