theory Arch imports Main "HOL-Library.Code_Target_Numeral" begin
setup‹fn thy =>
let
val T = @{typ "integer list list list"}
val dir = Resources.master_directory thy
in
thy |>
Code_Runtime.polyml_as_definition
[(@{binding Tri'}, T), (@{binding Quad'}, T), (@{binding Pent'}, T),
(@{binding Hex'}, T)]
(map (Path.append dir)
[🍋‹Archives/Tri.ML›, 🍋‹Archives/Quad.ML›, 🍋‹Archives/Pent.ML›, 🍋‹Archives/Hex.ML›])
end ›
text‹The definition of these constants is only ever needed at the ML level
running the eval proof method.›
definition Tri :: "nat list list list" where "Tri = (map ∘ map ∘ map) nat_of_integer Tri'"
definition Quad :: "nat list list list" where "Quad = (map ∘ map ∘ map) nat_of_integer Quad'"
definition Pent :: "nat list list list" where "Pent = (map ∘ map ∘ map) nat_of_integer Pent'"
definition Hex :: "nat list list list" where "Hex = (map ∘ map ∘ map) nat_of_integer Hex'"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
