Commit 3bc91de3 authored by Alexander Bentkamp's avatar Alexander Bentkamp
Browse files

interpretations for locales in deep learning

--HG--
branch : deep_learning
parent 0b99a44c62fb
......@@ -933,4 +933,13 @@ lemma witness_det: "det (submatrix Aw' rows_with_1 rows_with_1) \<noteq> 0" unfo
end
(* Examples to show that the locales can be instantiated: *)
interpretation example : deep_model_correct_params "[10,10,10]"
unfolding deep_model_correct_params_def by simp
interpretation example : deep_model_correct_params_y "[10,10,10]" 1
unfolding deep_model_correct_params_y_def deep_model_correct_params_y_axioms_def
deep_model_correct_params_def by simp
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment