Built with Alectryon. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
Hover-Settings: Show types: Show goals:
import Lean
import Playground.Zulip.EnvExInit

open Lean Meta Elab Command Tactic

error: unsolved goals ⊢ 1 + 2 = 3

Error: ❌️ Docstring on `#guard_msgs` does not match generated message:

error: unsolved goals
⊢ 1 + 2 = 3
 in
theorem 
foo: 1 + 2 = 3
foo : 
1: Nat
1 + 
2: Nat
2 = 
3: Nat
3 := 
Error: unsolved goals
⊢ 1 + 2 = 3
1 + 2 = 3

  
Error: unsolved goals
⊢ 1 + 2 = 3
1 + 2 = 3