Module 1 · Level 1

The Infoview Panel

The Infoview is your live feedback dashboard. It shows evaluation results, goals, and types without leaving your editor.

What You See in the Infoview

Whenever your cursor is on a line, Lean reports the type of the expression, any errors, and the current goal if you are inside a proof.

lean

1def triple (x : Nat) : Nat := x * 3
2#check triple
3#eval triple 4

💡

The Infoview updates as you move your cursor. Hover over expressions to see types even without writing #check.

Lean tells you the expected type and the actual type. Use that to correct mismatches.

lean

1def badAdd : Nat := "oops"
2-- Lean reports: expected Nat, got String

Key Takeaway

The Infoview is your main debugging tool. Keep it open and scan it constantly.