mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
83 lines
1.3 KiB
Lean4
83 lines
1.3 KiB
Lean4
/-!
|
|
Tests the behavior of string interpolation literals
|
|
-/
|
|
|
|
/-!
|
|
Constant values are correctly interpolated.
|
|
-/
|
|
|
|
#eval s!"hello {1+1}"
|
|
|
|
/-!
|
|
Values with variables are correctly interpolated.
|
|
-/
|
|
|
|
def tst (x : Nat) : IO Unit := do
|
|
IO.println s!"x: {x}"
|
|
IO.println s!"x+1: {x+1}"
|
|
|
|
/--
|
|
info: x: 10
|
|
x+1: 11
|
|
-/
|
|
#guard_msgs in
|
|
#eval tst 10
|
|
|
|
/-!
|
|
Opening braces (`{`) can be escaped, closing braces (`}`) don't need to be.
|
|
-/
|
|
|
|
/-- info: "{2}" -/
|
|
#guard_msgs in
|
|
#eval s!"\{{1+1}}"
|
|
|
|
/-!
|
|
String interpolation doesn't add any spaces.
|
|
-/
|
|
|
|
/-- info: "1+1" -/
|
|
#guard_msgs in
|
|
#eval s!"{1}+{1}"
|
|
|
|
/-- info: "a1" -/
|
|
#guard_msgs in
|
|
#eval s!"a{1}"
|
|
|
|
/-!
|
|
String interpolation works correctly with monadic computations.
|
|
-/
|
|
|
|
def g (x : Nat) : StateRefT Nat IO Nat := do
|
|
modify (· + x)
|
|
get
|
|
|
|
def ex : StateRefT Nat IO Unit := do
|
|
IO.println s!">> hello {← g 1}"
|
|
IO.println s!">> world {← g 1}"
|
|
|
|
/--
|
|
info: >> hello 1
|
|
>> world 2
|
|
-/
|
|
#guard_msgs in
|
|
#eval ex.run' 0
|
|
|
|
/-!
|
|
String interpolation elaborates to the individual components wrapped in `toString` and combined
|
|
using `++`.
|
|
-/
|
|
|
|
/--
|
|
info: toString "he" ++ toString "llo" ++ toString ", " ++ toString "wo" ++ toString "rld" : String
|
|
-/
|
|
#guard_msgs in
|
|
#check s!"he{"llo"}, {"wo"}rld"
|
|
|
|
/-!
|
|
Redundant parts are omitted.
|
|
-/
|
|
|
|
/-- info: toString 1 ++ toString 2 : String -/
|
|
#guard_msgs in
|
|
#check s!"{1}{2}"
|