Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] code-relect features

view this post on Zulip Email Gateway (Aug 18 2022 at 20:09):

From: Christian Urban <christian.urban@kcl.ac.uk>
Dear Yongjian,

For this example to work you need to include the theory

"~~/src/HOL/Library/Efficient_Nat"

in the imports-section of your theory.

Hope this helps,
Christian

view this post on Zulip Email Gateway (Aug 18 2022 at 20:28):

From: li yongjian <lyj238@gmail.com>
Dear urban:

I'm trying the code_reflect features.

But there is still type erros.

COuld you please take time to view it.

See attachment
machineLearning.thy

Last updated: Nov 21 2024 at 12:39 UTC