Display the input term in the output of the Check command. It is useful to see the fully elaborated term.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/lean_parser.cpp

@@ -1201,7 +1201,11 @@ class parser::imp {
         next();
         expr v = m_elaborator(parse_expr());
         expr t = infer_type(v, m_frontend);
-        regular(m_frontend) << t << endl;
+        formatter fmt = m_frontend.get_state().get_formatter();
+        options opts  = m_frontend.get_state().get_options();
+        unsigned indent = get_pp_indent(opts);
+        format r = group(format{fmt(v), space(), colon(), nest(indent, compose(line(), fmt(t)))});
+        regular(m_frontend) << mk_pair(r, opts) << endl;
     }
 
     /** \brief Return the (optional) precedence of a user-defined operator. */

tests/lean/arith1.lean.expected.out

@@ -1,11 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
-ℕ
-ℕ
-ℤ
+10 + 20 : ℕ
+10 : ℕ
+10 - 20 : ℤ
 -10
 5
-ℤ
+15 + 10 - 20 : ℤ
   Assumed: x
   Assumed: n
   Assumed: m

tests/lean/cast1.lean.expected.out

@@ -13,4 +13,4 @@ Function type:
 Arguments types:
     m : ℕ
     v1 : vector ℤ (m + 0)
-ℤ
+f m (cast (V0 ℤ m) v1) : ℤ

tests/lean/cast2.lean.expected.out

@@ -6,7 +6,7 @@
   Assumed: B'
   Assumed: H
   Assumed: a
-A = A'
+DomInj H : A = A'
   Proved: BeqB'
   Set: lean::pp::implicit
 DomInj::explicit A A' (λ x : A, B) (λ x : A', B') H

tests/lean/cast3.lean.expected.out

@@ -15,7 +15,7 @@ b
   Assumed: H2
   Defined: g
 0
-ℕ
+g (cast H2 f a') : ℕ
 Cast B B' (RanInj H2 (Cast A' A (Symm (DomInj H2)) a')) b
   Assumed: A1
   Assumed: A2
@@ -24,4 +24,4 @@ Cast B B' (RanInj H2 (Cast A' A (Symm (DomInj H2)) a')) b
   Assumed: Hb
   Assumed: a
 Cast A1 A3 (Trans Hb Ha) a
-A3
+cast Hb (cast Ha a) : A3

tests/lean/coercion2.lean.expected.out

@@ -22,8 +22,8 @@ g b (t2r a)
   Set: lean::pp::notation
 g (g a b) a
 h (h r s) r
-R
-S
+a ++ b ++ a : R
+r ++ s ++ r : S
   Set: lean::pp::coercion
 g (g (t2r a) b) (t2r a)
 h (h r s) r

tests/lean/elab5.lean

@@ -0,0 +1,12 @@
+Variable C {A B : Type} (H : A = B) (a : A) : B
+
+Variable D {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) : A = A'
+
+Variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A) :
+             (B a) = (B' (C (D H) a))
+
+Theorem R2 : Pi (A1 A2 B1 B2 : Type), (A1 -> B1 = A2 -> B2) -> A1 -> (B1 = B2) :=
+    fun A1 A2 B1 B2 H a, R H a
+
+Set pp::implicit true
+Show Environment 7.

tests/lean/elab5.lean.expected.out

@@ -0,0 +1,23 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: C
+  Assumed: D
+  Assumed: R
+  Proved: R2
+  Set: lean::pp::implicit
+Variable C {A B : Type} (H : A = B) (a : A) : B
+Definition C::explicit (A B : Type) (H : A = B) (a : A) : B := C H a
+Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) : A = A'
+Definition D::explicit (A A' : Type) (B : A → Type) (B' : A' → Type) (H : (Π x : A, B x) = (Π x : A', B' x)) : A =
+    A' :=
+    D H
+Variable R {A A' : Type} {B : A → Type} {B' : A' → Type} (H : (Π x : A, B x) = (Π x : A', B' x)) (a : A) :
+    (B a) = (B' (C::explicit A A' (D::explicit A A' B B' H) a))
+Definition R::explicit (A A' : Type)
+    (B : A → Type)
+    (B' : A' → Type)
+    (H : (Π x : A, B x) = (Π x : A', B' x))
+    (a : A) : (B a) = (B' (C (D H) a)) :=
+    R H a
+Theorem R2 (A1 A2 B1 B2 : Type) (H : A1 → B1 = A2 → B2) (a : A1) : B1 = B2 :=
+    R::explicit A1 A2 (λ _ : A1, B1) (λ _ : A2, B2) H a

tests/lean/let1.lean.expected.out

@@ -6,9 +6,9 @@ let a : ℕ := 1000000000000000000,
     c : ℕ := 3000000000000000000,
     d : ℕ := 4000000000000000000
 in a + b + c + d
-ℕ
+let a : ℕ := 10 in a + 1 : ℕ
 30
 30
-ℤ
+let a : ℤ := 20 in a + 10 : ℤ
   Set: lean::pp::coercion
 let a : ℤ := nat_to_int 20 in a + (nat_to_int 10)

tests/lean/let4.lean.expected.out

@@ -6,15 +6,15 @@ Given type:
     Bool
   Assumed: vector
   Assumed: const
-vector Bool 10
+let a := 10, v1 := const a ⊤, v2 := v1 in v2 : vector Bool 10
 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2
-vector Bool 10
+let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector Bool a := v1 in v2 : vector Bool 10
 Error (line: 31, pos: 26) type mismatch at definition 'v2', expected type
     vector ℤ a
 Given type:
     vector Bool a
   Assumed: foo
   Coercion foo
-vector ℤ 10
+let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := v1 in v2 : vector ℤ 10
   Set: lean::pp::coercion
 let a := 10, v1 : vector Bool a := const a ⊤, v2 : vector ℤ a := foo v1 in v2

tests/lean/tst1.lean.expected.out

@@ -25,15 +25,15 @@ Definition map {A B C : Type} {n : N} (f : A → B → C) (v1 : vector A n) (v2
     λ (i : N) (H : i < n), f (v1 i H) (v2 i H)
 Definition map::explicit (A B C : Type) (n : N) (f : A → B → C) (v1 : vector A n) (v2 : vector B n) : vector C n :=
     map f v1 v2
-Bool
+select (update (const three ⊥) two ⊤) two two_lt_three : Bool
 ⊤
-vector Bool three
+update (const three ⊥) two ⊤ : vector Bool three
 
 --------
-Π (A : Type) (n : N) (v : vector A n) (i : N), (i < n) → A
+select::explicit : Π (A : Type) (n : N) (v : vector A n) (i : N), (i < n) → A
 
 map type ---> 
-Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
+map::explicit : Π (A B C : Type) (n : N), (A → B → C) → (vector A n) → (vector B n) → (vector C n)
 
 map normal form --> 
 λ (A B C : Type)

tests/lean/tst10.lean.expected.out

@@ -14,11 +14,11 @@ a ∨ b
 a ∨ b
 a ∨ a ∨ b
 a ⇒ b ⇒ a
-Bool
+a ⇒ b : Bool
 if Bool a a ⊤
 a
   Assumed: H1
   Assumed: H2
-Π (a b : Bool), (a ⇒ b) → a → b
+MP::explicit : Π (a b : Bool), (a ⇒ b) → a → b
 MP H2 H1
-b
+MP H2 H1 : b

tests/lean/tst11.lean.expected.out

@@ -6,7 +6,7 @@
 ⊤
   Assumed: a
 a ⊕ a ⊕ a
-Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b)
+Subst::explicit : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b)
   Proved: EM2
-Π a : Bool, a ∨ ¬ a
-a ∨ ¬ a
+EM2 : Π a : Bool, a ∨ ¬ a
+EM2 a : a ∨ ¬ a

tests/lean/tst14.lean.expected.out

@@ -3,5 +3,5 @@
 ℤ → ℤ → ℤ
   Assumed: f
 f 0
-ℤ → ℤ
-ℤ
+f 0 : ℤ → ℤ
+f 0 1 : ℤ

tests/lean/tst15.lean.expected.out

@@ -1,22 +1,22 @@
   Set: pp::colors
   Set: pp::unicode
   Assumed: x
-Type U+3 ⊔ M+2 ⊔ 3
+x : Type U+3 ⊔ M+2 ⊔ 3
   Assumed: f
-Type U+10 → Type
-Type
-Type 5
-Type U+3 ⊔ M+2 ⊔ 3
-Type U+1 ⊔ M+1
+f : Type U+10 → Type
+f x : Type
+Type 4 : Type 5
+x : Type U+3 ⊔ M+2 ⊔ 3
+Type U ⊔ M : Type U+1 ⊔ M+1
 Type U+3
-Type U+4
-Type U+1 ⊔ M+1
-Type U+1 ⊔ M+1 ⊔ 4
+Type U+3 : Type U+4
+Type U ⊔ M : Type U+1 ⊔ M+1
+Type U ⊔ M ⊔ 3 : Type U+1 ⊔ M+1 ⊔ 4
 Type U+1 ⊔ M ⊔ 3
-Type U+2 ⊔ M+1 ⊔ 4
+Type U+1 ⊔ M ⊔ 3 : Type U+2 ⊔ M+1 ⊔ 4
 Type U → Type 5
-Type U+1 ⊔ 6
-Type M+1 ⊔ 4 ⊔ U+6
+Type U → Type 5 : Type U+1 ⊔ 6
+Type M ⊔ 3 → Type U+5 : Type M+1 ⊔ 4 ⊔ U+6
 Type M ⊔ 3 → Type U → Type 5
-Type M+1 ⊔ 6 ⊔ U+1
+Type M ⊔ 3 → Type U → Type 5 : Type M+1 ⊔ 6 ⊔ U+1
 Type U

tests/lean/tst16.lean.expected.out

@@ -6,7 +6,7 @@
 ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
 ∃ (a b : Type) (c : Bool), g c ((f a) = (f b))
 ∀ (a b : Type) (c : Bool), (g c (f a)) = (f b) ⇒ (f a)
-Bool
+∀ (a b : Type) (c : Bool), g c ((f a) = (f b)) : Bool
 ∀ (a b : Type) (c : Bool), g c ((f a) = (f b))
 ∀ a b : Type, (f a) = (f b)
 ∃ a b : Type, (f a) = (f b) ∧ (f a)

tests/lean/tst17.lean.expected.out

@@ -3,7 +3,7 @@
   Assumed: f
   Assumed: g
 ∀ a b : Type, ∃ c : Type, (g a b) = (f c)
-Bool
+∀ a b : Type, ∃ c : Type, (g a b) = (f c) : Bool
 (λ a : Type,
    (λ b : Type, if Bool ((λ x : Type, if Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
    (λ x : Type, ⊤)) =

tests/lean/tst4.lean.expected.out

@@ -9,8 +9,9 @@ f::explicit N n1 n2
 f::explicit ((N → N) → N → N) (λ x : N → N, x) (λ y : N → N, y)
   Assumed: EqNice
 EqNice::explicit N n1 n2
-N
-Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
+f n1 n2 : N
+Congr::explicit :
+    Π (A : Type U) (B : A → Type U) (f g : Π x : A, B x) (a b : A), (f = g) → (a = b) → ((f a) = (g b))
 f::explicit N n1 n2
   Assumed: a
   Assumed: b

tests/lean/tst5.lean.expected.out

@@ -4,7 +4,7 @@
   Assumed: a
   Assumed: b
 a ≃ b
-Bool
+a ≃ b : Bool
   Set: lean::pp::implicit
 heq::explicit N a b
 heq::explicit Type 2 Type 1 Type 1

tests/lean/tst7.lean.expected.out

@@ -13,7 +13,8 @@ Elaborator state
     #0 ≈ lift:0:2 ?M0
   Assumed: myeq
 myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b)
-Bool
+myeq (Π (A : Type), A → A) (λ (A : Type) (a : A), a) (λ (B : Type) (b : B), b) : Bool
   Assumed: R
   Assumed: h
-Bool → (Π (f1 g1 : Π A : Type, R A), (Π A : Type, myeq (R A) (f1 A) (g1 A)) → Bool)
+λ (H : Bool) (f1 g1 : Π A : Type, R A) (G : Π A : Type, myeq (R A) (f1 A) (g1 A)), h f1 :
+    Bool → (Π (f1 g1 : Π A : Type, R A), (Π A : Type, myeq (R A) (f1 A) (g1 A)) → Bool)

tests/lean/tst8.lean.expected.out

@@ -1,6 +1,6 @@
   Set: pp::colors
   Set: pp::unicode
-Π (A : Type), A → A
+λ (A : Type) (a : A), let b := a in b : Π (A : Type), A → A
   Assumed: g
   Defined: f
 f ℕ 10