/- This is a lean(4) file to test Lean syntax highlighting -/
-- import
import Mathlib.Data.Int.Basic
import Mathlib.Tactic.Ring

/-! Multiline
      doc comments -/
#check 1
/- comment and
/- /- nested -/
comment-/
-/

-- bool
#check true && false

-- String, with escape and linebreak
#print "String: Line1\nLine2 and \" quote mark \r\nLine3 and \\ backslash
Line\u0034"

def name_with_number_1234: ℕ := 1
def «test_flqq&frqq+2333»: ℕ := 2333
-- Decimal, Hexadecimal, Decimal
#reduce name_with_number_1234+«test_flqq&frqq+2333»+10 + 0x0011 + 00001
-- Float
#eval 1.1+1.1E1+1e1+0.1E2+22E-1+0.0E-0-0

--namesoace
namespace test

-- theorem with modifiers 
@[simp] private theorem test_modifiers: 1+1=2 := by
  /- use tactic -/
  let one_add_one_eq_two := show 1+1=2 from by simp
  exact one_add_one_eq_two

lemma test_sorry: 1+2=3 := by
  -- sorry or admit
  sorry

end test