1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
import Init namespace Sample /-- A theorem left open. -/ theorem foo (n : Nat) : n = n := by sorry def bar : Nat := by admit theorem baz : True := by trivial end Sample