git.iko.soy/bat
on master help sign in
Add a Lean highlighting test file.
af8a803Julian Berman
tests/syntax-tests/highlighted/Lean/test.leannew file+68
compare with master
unifiedsplit
@@ -0,0 +1,68 @@
1+import data.matrix.notation
2+import data.vector2
3+
4+/-!
5+
6+Helpers that don't currently fit elsewhere...
7+
8+-/
9+
10+lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
11+ p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
12+
13+-- For `playfield`s, the piece type and/or piece index type.
14+variables (X : Type*)
15+variables [has_repr X]
16+
17+namespace chess.utils
18+
19+section repr
20+
21+/--
22+An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
23+for `option`, and rather, output just the value in the `some` and a custom provided
24+`string` for `none`.
25+-/
26+structure option_wrapper :=
27+(val : option X)
28+(none_s : string)
29+
30+instance wrapped_option_repr : has_repr (option_wrapper X) :=
31+⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
32+
33+variables {X}
34+/--
35+Construct an `option_wrapper` term from a provided `option X` and the `string`
36+that will override the `has_repr.repr` for `none`.
37+-/
38+def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
39+
40+-- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
41+variables {m' n' : ℕ}
42+
43+/--
44+For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
45+the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
46+This definition is used for displaying rows of the playfield, when it is defined
47+via a `matrix`, likely through notation.
48+-/
49+def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
50+λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
51+
52+instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
53+
54+/--
55+For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
56+we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
57+This definition is used for displaying the playfield, when it is defined
58+via a `matrix`, likely through notation.
59+-/
60+def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
61+λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
62+
63+instance matrix_repr_instance :
64+ has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
65+
66+end repr
67+
68+end chess.utils
tests/syntax-tests/source/Lean/test.leannew file+68
@@ -0,0 +1,68 @@
1+import data.matrix.notation
2+import data.vector2
3+
4+/-!
5+
6+Helpers that don't currently fit elsewhere...
7+
8+-/
9+
10+lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
11+ p = x ∨ p' = x ∨ (x ≠ p ∧ x ≠ p') := by tauto
12+
13+-- For `playfield`s, the piece type and/or piece index type.
14+variables (X : Type*)
15+variables [has_repr X]
16+
17+namespace chess.utils
18+
19+section repr
20+
21+/--
22+An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
23+for `option`, and rather, output just the value in the `some` and a custom provided
24+`string` for `none`.
25+-/
26+structure option_wrapper :=
27+(val : option X)
28+(none_s : string)
29+
30+instance wrapped_option_repr : has_repr (option_wrapper X) :=
31+⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
32+
33+variables {X}
34+/--
35+Construct an `option_wrapper` term from a provided `option X` and the `string`
36+that will override the `has_repr.repr` for `none`.
37+-/
38+def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
39+
40+-- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
41+variables {m' n' : ℕ}
42+
43+/--
44+For a "vector" `X^n'` represented by the type `Π n' : ℕ, fin n' → X`, where
45+the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
46+This definition is used for displaying rows of the playfield, when it is defined
47+via a `matrix`, likely through notation.
48+-/
49+def vec_repr : Π {n' : ℕ}, (fin n' → X) → string :=
50+λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
51+
52+instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
53+
54+/--
55+For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
56+we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
57+This definition is used for displaying the playfield, when it is defined
58+via a `matrix`, likely through notation.
59+-/
60+def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
61+λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
62+
63+instance matrix_repr_instance :
64+ has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
65+
66+end repr
67+
68+end chess.utils