Stream: Beginner Questions

Topic: Missing theory context

Julin Shaji (Feb 12 2025 at 06:15):

I was trying my first isabelle proof like this:

theory ONat
  imports Main
begin

datatype onat = Zero | Succ onat

fun oadd :: "onat ⇒ onat ⇒ onat" where
  "oadd Zero n = n" |
  "oadd (Succ m) n = Succ (oadd m n)"
end

lemma add_O2: "oadd m Zero = m"
  apply (induction m)

At this stage I got an error saying this:

Outer syntax error⌂: missing theory context for command "apply"

Does this mean that I need to make a new theory?

Mathias Fleury (Feb 12 2025 at 06:59):

There is no end after fun

Mathias Fleury (Feb 12 2025 at 06:59):

Isabelle uses the | to know when the declaration ends

Julin Shaji (Feb 12 2025 at 07:22):

Thanks.

That end was supposed to be for ending the theory and somehow got there in between.

Last updated: Mar 09 2025 at 12:28 UTC