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