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

  Set: pp::colors
  Set: pp::unicode
  Assumed: f
Failed to solve
 ⊢ (?M::1 ≈ λ x : ℕ, x) ⊕ (?M::1 ≈ nat_to_int) ⊕ (?M::1 ≈ nat_to_real)
    (line: 4: pos: 8) Coercion for
        10
    Failed to solve
     ⊢ Bool ≺ ℕ
        Substitution
         ⊢ Bool ≺ ?M::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M::0
                ?M::1 10
                ⊤
            Assignment
             ⊢ ℕ ≺ ?M::0
                Substitution
                 ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M::0
                        ?M::1 10
                        ⊤
                    Assignment
                    x : ℕ ⊢ ℕ ≈ ?M::5
                        Destruct/Decompose
                         ⊢ ℕ → ℕ ≈ Π x : ?M::4, ?M::5
                            Substitution
                             ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
                                 Function expected at
                                    ?M::1 10
                                Assignment
                                 ⊢ ℕ → ℕ ≺ ?M::3
                                    Propagate type, ?M::1 : ?M::3
                                        Assignment
                                         ⊢ ?M::1 ≈ λ x : ℕ, x
                                            Assumption 0
    Failed to solve
     ⊢ Bool ≺ ℤ
        Substitution
         ⊢ Bool ≺ ?M::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M::0
                ?M::1 10
                ⊤
            Assignment
             ⊢ ℤ ≺ ?M::0
                Substitution
                 ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M::0
                        ?M::1 10
                        ⊤
                    Assignment
                    a : ℕ ⊢ ℤ ≈ ?M::5
                        Destruct/Decompose
                         ⊢ ℕ → ℤ ≈ Π x : ?M::4, ?M::5
                            Substitution
                             ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
                                 Function expected at
                                    ?M::1 10
                                Assignment
                                 ⊢ ℕ → ℤ ≺ ?M::3
                                    Propagate type, ?M::1 : ?M::3
                                        Assignment
                                         ⊢ ?M::1 ≈ nat_to_int
                                            Assumption 1
    Failed to solve
     ⊢ Bool ≺ ℝ
        Substitution
         ⊢ Bool ≺ ?M::0
            (line: 4: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M::0
                ?M::1 10
                ⊤
            Assignment
             ⊢ ℝ ≺ ?M::0
                Substitution
                 ⊢ ?M::5[inst:0 (10)] ≺ ?M::0
                    (line: 4: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                        f::explicit
                    with arguments:
                        ?M::0
                        ?M::1 10
                        ⊤
                    Assignment
                    a : ℕ ⊢ ℝ ≈ ?M::5
                        Destruct/Decompose
                         ⊢ ℕ → ℝ ≈ Π x : ?M::4, ?M::5
                            Substitution
                             ⊢ ?M::3 ≈ Π x : ?M::4, ?M::5
                                 Function expected at
                                    ?M::1 10
                                Assignment
                                 ⊢ ℕ → ℝ ≺ ?M::3
                                    Propagate type, ?M::1 : ?M::3
                                        Assignment
                                         ⊢ ?M::1 ≈ nat_to_real
                                            Assumption 2
  Assumed: g
Error (line: 7, pos: 8) invalid expression, it still contains metavariables after elaboration, metavariable: ?M::1, type:
Type
  Assumed: h
Failed to solve
x : ?M::0, A : Type ⊢ ?M::0 ≺ 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: my_eq
Failed to solve
A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
    (line: 15: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
        my_eq
    with arguments:
        C
        a
        b
  Assumed: a
  Assumed: b
  Assumed: H
Failed to solve
 ⊢ ?M::0 ⇒ ?M::3 ∧ a ≺ b
    Substitution
     ⊢ ?M::0 ⇒ ?M::1 ≺ b
        (line: 20: pos: 18) Type of definition 't1' must be convertible to expected type.
        Assignment
        H1 : ?M::2 ⊢ ?M::3 ∧ a ≺ ?M::1
            Substitution
            H1 : ?M::2 ⊢ ?M::3 ∧ ?M::4 ≺ ?M::1
                Destruct/Decompose
                 ⊢ Π H1 : ?M::2, ?M::3 ∧ ?M::4 ≺ Π a : ?M::0, ?M::1
                    (line: 20: pos: 18) Type of argument 3 must be convertible to the expected type in the application of
                        Discharge::explicit
                    with arguments:
                        ?M::0
                        ?M::1
                        λ H1 : ?M::2, Conj H1 (Conjunct1 H)
                Assignment
                H1 : ?M::2 ⊢ a ≺ ?M::4
                    Substitution
                    H1 : ?M::2 ⊢ ?M::5 ≺ ?M::4
                        (line: 20: pos: 37) Type of argument 4 must be convertible to the expected type in the application of
                            Conj::explicit
                        with arguments:
                            ?M::3
                            ?M::4
                            H1
                            Conjunct1 H
                        Assignment
                        H1 : ?M::2 ⊢ a ≈ ?M::5
                            Destruct/Decompose
                            H1 : ?M::2 ⊢ a ∧ b ≺ ?M::5 ∧ ?M::6
                                (line: 20: pos: 45) Type of argument 3 must be convertible to the expected type in the application of
                                    Conjunct1::explicit
                                with arguments:
                                    ?M::5
                                    ?M::6
                                    H
Failed to solve
 ⊢ b ≈ a
    Substitution
     ⊢ b ≈ ?M::3
        Destruct/Decompose
         ⊢ b == b ≺ ?M::3 == ?M::4
            (line: 22: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
                Trans::explicit
            with arguments:
                ?M::1
                ?M::2
                ?M::3
                ?M::4
                Refl a
                Refl b
        Assignment
         ⊢ a ≈ ?M::3
            Destruct/Decompose
             ⊢ a == a ≺ ?M::2 == ?M::3
                (line: 22: pos: 22) Type of argument 5 must be convertible to the expected type in the application of
                    Trans::explicit
                with arguments:
                    ?M::1
                    ?M::2
                    ?M::3
                    ?M::4
                    Refl a
                    Refl b
Failed to solve
 ⊢ (?M::1 ≈ Type) ⊕ (?M::1 ≈ Bool)
    Destruct/Decompose
     ⊢ ?M::1 ≺ Type
        (line: 24: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
            f::explicit
        with arguments:
            ?M::0
            Bool
            Bool
    Failed to solve
     ⊢
    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
        Destruct/Decompose
         ⊢ Type ≺ ?M::0
            (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M::0
                Bool
                Bool
        Failed to solve
         ⊢ (Type 1) ≺ Type
            Substitution
             ⊢ (Type 1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ Type
                        Assumption 1
                Assignment
                 ⊢ ?M::1 ≈ Type
                    Assumption 0
        Failed to solve
         ⊢ (Type 2) ≺ Type
            Substitution
             ⊢ (Type 2) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type 1)
                        Assumption 2
                Assignment
                 ⊢ ?M::1 ≈ Type
                    Assumption 0
        Failed to solve
         ⊢ (Type 3) ≺ Type
            Substitution
             ⊢ (Type 3) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type 2)
                        Assumption 3
                Assignment
                 ⊢ ?M::1 ≈ Type
                    Assumption 0
        Failed to solve
         ⊢ (Type M+1) ≺ Type
            Substitution
             ⊢ (Type M+1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type M)
                        Assumption 4
                Assignment
                 ⊢ ?M::1 ≈ Type
                    Assumption 0
        Failed to solve
         ⊢ (Type U+1) ≺ Type
            Substitution
             ⊢ (Type U+1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type U)
                        Assumption 5
                Assignment
                 ⊢ ?M::1 ≈ Type
                    Assumption 0
    Failed to solve
     ⊢
    (?M::0 ≈ Type) ⊕ (?M::0 ≈ (Type 1)) ⊕ (?M::0 ≈ (Type 2)) ⊕ (?M::0 ≈ (Type M)) ⊕ (?M::0 ≈ (Type U))
        Destruct/Decompose
         ⊢ Type ≺ ?M::0
            (line: 24: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
                f::explicit
            with arguments:
                ?M::0
                Bool
                Bool
        Failed to solve
         ⊢ (Type 1) ≺ Bool
            Substitution
             ⊢ (Type 1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ Type
                        Assumption 7
                Assignment
                 ⊢ ?M::1 ≈ Bool
                    Assumption 6
        Failed to solve
         ⊢ (Type 2) ≺ Bool
            Substitution
             ⊢ (Type 2) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type 1)
                        Assumption 8
                Assignment
                 ⊢ ?M::1 ≈ Bool
                    Assumption 6
        Failed to solve
         ⊢ (Type 3) ≺ Bool
            Substitution
             ⊢ (Type 3) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type 2)
                        Assumption 9
                Assignment
                 ⊢ ?M::1 ≈ Bool
                    Assumption 6
        Failed to solve
         ⊢ (Type M+1) ≺ Bool
            Substitution
             ⊢ (Type M+1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type M)
                        Assumption 10
                Assignment
                 ⊢ ?M::1 ≈ Bool
                    Assumption 6
        Failed to solve
         ⊢ (Type U+1) ≺ Bool
            Substitution
             ⊢ (Type U+1) ≺ ?M::1
                Propagate type, ?M::0 : ?M::1
                    Assignment
                     ⊢ ?M::0 ≈ (Type U)
                        Assumption 11
                Assignment
                 ⊢ ?M::1 ≈ Bool
                    Assumption 6
Failed to solve
a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ a
    Substitution
    a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ (a ⇒ b) ⇒ a ≺ ?M::5[lift:0:1]
        Substitution
        a : Bool, b : Bool, H : ?M::2, H_a : ?M::6 ⊢ ?M::2[lift:0:2] ≺ ?M::5[lift:0:1]
            Destruct/Decompose
            a : Bool, b : Bool, H : ?M::2 ⊢ Π H_a : ?M::6, ?M::2[lift:0:2] ≺ Π a : ?M::3, ?M::5[lift:0:1]
                (line: 27: pos: 21) Type of argument 5 must be convertible to the expected type in the application of
                    DisjCases::explicit
                with arguments:
                    ?M::3
                    ?M::4
                    ?M::5
                    EM a
                    λ H_a : ?M::6, H
                    λ H_na : ?M::7, NotImp1 (MT H H_na)
             Normalize assignment
                ?M::0
                Assignment
                a : Bool, b : Bool ⊢ ?M::2 ≈ ?M::0
                    Destruct/Decompose
                    a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
                        (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
                            Discharge::explicit
                        with arguments:
                            ?M::0
                            ?M::1
                            λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
                Assignment
                a : Bool, b : Bool ⊢ ?M::0 ≈ (a ⇒ b) ⇒ a
                    Destruct/Decompose
                    a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
                        Destruct/Decompose
                        a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
                            Destruct/Decompose
                             ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
                                (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.
        Assignment
        a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ a
            Substitution
            a : Bool, b : Bool, H : ?M::2 ⊢ ?M::5 ≺ ?M::1[lift:0:1]
                Destruct/Decompose
                a : Bool, b : Bool ⊢ Π H : ?M::2, ?M::5 ≺ Π a : ?M::0, ?M::1[lift:0:1]
                    (line: 27: pos: 4) Type of argument 3 must be convertible to the expected type in the application of
                        Discharge::explicit
                    with arguments:
                        ?M::0
                        ?M::1
                        λ H : ?M::2, DisjCases (EM a) (λ H_a : ?M::6, H) (λ H_na : ?M::7, NotImp1 (MT H H_na))
                Assignment
                a : Bool, b : Bool ⊢ ?M::1 ≈ a
                    Destruct/Decompose
                    a : Bool, b : Bool ⊢ ?M::0 ⇒ ?M::1 ≺ ((a ⇒ b) ⇒ a) ⇒ a
                        Destruct/Decompose
                        a : Bool ⊢ Π b : Bool, ?M::0 ⇒ ?M::1 ≺ Π b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
                            Destruct/Decompose
                             ⊢ Π a b : Bool, ?M::0 ⇒ ?M::1 ≺ Π a b : Bool, ((a ⇒ b) ⇒ a) ⇒ a
                                (line: 26: pos: 16) Type of definition 'pierce' must be convertible to expected type.