lean2/tests/lean/elab1.lean.expected.out

  Set: pp::colors
  Set: pp::unicode
  Assumed: f
Failed to solve
 ⊢ (?M3::1 ≈ λ x : ℕ, x) ⊕ (?M3::1 ≈ nat_to_int) ⊕ (?M3::1 ≈ nat_to_real)
    (line: 4: pos: 8) Coercion for
        10
    Failed to solve
     ⊢ Bool ≺ ℕ
        Substitution
         ⊢ Bool ≺ ?M3::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M3::0
                ?M3::1 10
                ⊤
            Assignment
             ⊢ ℕ ≺ ?M3::0
                Substitution
                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M3::0
                        ?M3::1 10
                        ⊤
                    Assignment
                    x : ℕ ⊢ λ x : ℕ, ℕ ≈ ?M3::5
                        Destruct/Decompose
                        x : ℕ ⊢ ℕ ≈ ?M3::5 x
                            Destruct/Decompose
                             ⊢ ℕ → ℕ ≈ Π x : ?M3::4, ?M3::5 x
                                Substitution
                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
                                     Function expected at
                                        ?M3::1 10
                                    Assignment
                                     ⊢ ℕ → ℕ ≺ ?M3::3
                                        Propagate type, ?M3::1 : ?M3::3
                                            Assignment
                                             ⊢ ?M3::1 ≈ λ x : ℕ, x
                                                assumption 0
    Failed to solve
     ⊢ Bool ≺ ℤ
        Substitution
         ⊢ Bool ≺ ?M3::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M3::0
                ?M3::1 10
                ⊤
            Assignment
             ⊢ ℤ ≺ ?M3::0
                Substitution
                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M3::0
                        ?M3::1 10
                        ⊤
                    Assignment
                    _ : ℕ ⊢ λ x : ℕ, ℤ ≈ ?M3::5
                        Destruct/Decompose
                        _ : ℕ ⊢ ℤ ≈ ?M3::5 _
                            Destruct/Decompose
                             ⊢ ℕ → ℤ ≈ Π x : ?M3::4, ?M3::5 x
                                Substitution
                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
                                     Function expected at
                                        ?M3::1 10
                                    Assignment
                                     ⊢ ℕ → ℤ ≺ ?M3::3
                                        Propagate type, ?M3::1 : ?M3::3
                                            Assignment
                                             ⊢ ?M3::1 ≈ nat_to_int
                                                assumption 1
    Failed to solve
     ⊢ Bool ≺ ℝ
        Substitution
         ⊢ Bool ≺ ?M3::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M3::0
                ?M3::1 10
                ⊤
            Assignment
             ⊢ ℝ ≺ ?M3::0
                Substitution
                 ⊢ (?M3::5[inst:0 (10)]) 10 ≺ ?M3::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M3::0
                        ?M3::1 10
                        ⊤
                    Assignment
                    _ : ℕ ⊢ λ x : ℕ, ℝ ≈ ?M3::5
                        Destruct/Decompose
                        _ : ℕ ⊢ ℝ ≈ ?M3::5 _
                            Destruct/Decompose
                             ⊢ ℕ → ℝ ≈ Π x : ?M3::4, ?M3::5 x
                                Substitution
                                 ⊢ ?M3::3 ≈ Π x : ?M3::4, ?M3::5 x
                                     Function expected at
                                        ?M3::1 10
                                    Assignment
                                     ⊢ ℕ → ℝ ≺ ?M3::3
                                        Propagate type, ?M3::1 : ?M3::3
                                            Assignment
                                             ⊢ ?M3::1 ≈ nat_to_real
                                                assumption 2
  Assumed: g
Error (line: 7, pos: 6) unsolved placeholder at term
    g 10
  Assumed: h
Failed to solve
x : ?M3::0, A : Type ⊢ ?M3::0[lift:0:2] ≺ A
    (line: 11: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
        h
    with arguments:
        A
        x
  Assumed: eq
Failed to solve
A : Type, B : Type, a : ?M3::0, b : ?M3::1, C : Type ⊢ ?M3::0[lift:0:3] ≺ C
    (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
        eq
    with arguments:
        C
        a
        b
  Assumed: a
  Assumed: b
  Assumed: H
Error (line: 20, pos: 18) type mismatch during term elaboration
    Discharge (λ H1 : _, Conj H1 (Conjunct1 H))
Term after elaboration:
    Discharge (λ H1 : ?M4, Conj H1 (Conjunct1 H))
Expected type:
    b
Got:
    ?M4 ⇒ ?M2
Elaborator state
    ?M2[lift:0:1] ≈ (?M4[lift:0:1]) ∧ a
    b ≈ if Bool ?M4 ?M2 ⊤
    b ≈ if Bool ?M4 ?M2 ⊤
Error (line: 22, pos: 22) type mismatch at application
    Trans (Refl a) (Refl b)
Function type:
    Π (A : Type U) (a b c : A), (a = b) → (b = c) → (a = c)
Arguments types:
    Bool : Type
    a : Bool
    a : Bool
    b : Bool
    Refl a : a = a
    Refl b : b = b
Error (line: 24, pos: 6) type mismatch at application
    f Bool Bool
Function type:
    Π (A : Type), A → A → A
Arguments types:
    Type : Type 1
    Bool : Type
    Bool : Type
Error (line: 27, pos: 21) type mismatch at application
    DisjCases (EM a) (λ H_a : a, H) (λ H_na : ¬ a, NotImp1 (MT H H_na))
Function type:
    Π (a b c : Bool), (a ∨ b) → (a → c) → (b → c) → c
Arguments types:
    a : Bool
    ¬ a : Bool
    a : Bool
    EM a : a ∨ ¬ a
    (λ H_a : a, H) : a → ((a ⇒ b) ⇒ a)
    (λ H_na : ¬ a, NotImp1 (MT H H_na)) : (¬ a) → a