bat/tests/syntax-tests/source/Lean/test.lean
2021-01-02 09:45:19 +01:00

69 lines
2.1 KiB
Plaintext
Vendored
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import data.matrix.notation
import data.vector2
/-!
Helpers that don't currently fit elsewhere...
-/
lemma split_eq {m n : Type*} (x : m × n) (p p' : m × n) :
p = x p' = x (x ≠ p ∧ x ≠ p') := by tauto
-- For `playfield`s, the piece type and/or piece index type.
variables (X : Type*)
variables [has_repr X]
namespace chess.utils
section repr
/--
An auxiliary wrapper for `option X` that allows for overriding the `has_repr` instance
for `option`, and rather, output just the value in the `some` and a custom provided
`string` for `none`.
-/
structure option_wrapper :=
(val : option X)
(none_s : string)
instance wrapped_option_repr : has_repr (option_wrapper X) :=
⟨λ ⟨val, s⟩, (option.map has_repr.repr val).get_or_else s⟩
variables {X}
/--
Construct an `option_wrapper` term from a provided `option X` and the `string`
that will override the `has_repr.repr` for `none`.
-/
def option_wrap (val : option X) (none_s : string) : option_wrapper X := ⟨val, none_s⟩
-- The size of the "vectors" for a `fin n' → X`, for `has_repr` definitions
variables {m' n' : }
/--
For a "vector" `X^n'` represented by the type `Π n' : , fin n' → X`, where
the `X` has a `has_repr` instance itself, we can provide a `has_repr` for the "vector".
This definition is used for displaying rows of the playfield, when it is defined
via a `matrix`, likely through notation.
-/
def vec_repr : Π {n' : }, (fin n' → X) → string :=
λ _ v, string.intercalate ", " ((vector.of_fn v).to_list.map repr)
instance vec_repr_instance : has_repr (fin n' → X) := ⟨vec_repr⟩
/--
For a `matrix` `X^(m' × n')` where the `X` has a `has_repr` instance itself,
we can provide a `has_repr` for the matrix, using `vec_repr` for each of the rows of the matrix.
This definition is used for displaying the playfield, when it is defined
via a `matrix`, likely through notation.
-/
def matrix_repr : Π {m' n'}, matrix (fin m') (fin n') X → string :=
λ _ _ M, string.intercalate ";\n" ((vector.of_fn M).to_list.map repr)
instance matrix_repr_instance :
has_repr (matrix (fin n') (fin m') X) := ⟨matrix_repr⟩
end repr
end chess.utils