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.
43 lines
1.0 KiB
Lean4
43 lines
1.0 KiB
Lean4
--
|
|
|
|
-- New notation that overlaps with existing notation
|
|
syntax (name := myPair) (priority := high) "(" term "," term ")" : term
|
|
|
|
macro_rules (kind := myPair)
|
|
| `(($a, $b)) => `([$a, $b])
|
|
|
|
#eval (1, 2) -- not ambiguous since myPair parser has higher priority
|
|
|
|
theorem ex1 : (1, 2) = [1, 2] :=
|
|
rfl
|
|
|
|
-- Define macro for expanding the builtin triple notation
|
|
-- Macros bypass builtin elaboration functions
|
|
macro_rules
|
|
| `(($a, $b, $c)) => `($a + $b + $c)
|
|
|
|
#eval (1, 2, 3)
|
|
|
|
syntax (name := mySingleton) "[" term "]" : term
|
|
|
|
macro_rules (kind := mySingleton)
|
|
| `([$a]) => `(2 * $a)
|
|
|
|
-- TODO: "ambiguous, possible interpretations" error messages print with
|
|
-- a lot of detail since most mvars have not been resolved yet
|
|
#check [1] -- ambiguous it can be `mySingleton` or the singleton list
|
|
|
|
|
|
syntax (priority := 100) "(" term "," term ", " term ")" : term -- priority without a kind
|
|
|
|
macro_rules
|
|
| `(($a, $b, $c)) => `([$a, $b, $c])
|
|
|
|
#eval (1,2,3)
|
|
|
|
theorem ex2 : (1, 2, 3) = [1, 2, 3] :=
|
|
rfl
|
|
|
|
theorem ex3 : (1, 2, 3, 4) = Prod.mk 1 (Prod.mk 2 (Prod.mk 3 4)) :=
|
|
rfl
|