Stream: General

Topic: How can I import AutoCorres?

view this post on Zulip KonjacSource (Dec 03 2023 at 22:51):

I'm taking a course which using AutoCorres. Our teacher offers the file below:
autocorres-1.10

And The templete use 

imports AutoCorres.AutoCorres

to import.

Which not work for me. Isabelle complains Bad theory import "AutoCorres.AutoCorres".

How can I import correctly?

view this post on Zulip Mathias Fleury (Dec 04 2023 at 05:56):

My guess: you have AutoCorres by forgot to tell Isabelle where it is. Do it like the AFP https://www.isa-afp.org/help/, but with the path to AutoCorres obviously.

view this post on Zulip KonjacSource (Dec 04 2023 at 10:59):

Mathias Fleury said:

My guess: you have AutoCorres by forgot to tell Isabelle where it is. Do it like the AFP https://www.isa-afp.org/help/, but with the path to AutoCorres obviously.

Thank you!!!!!! That works for me. :smiling_face_with_hearts:

Last updated: Dec 21 2024 at 12:33 UTC