Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Failed to parse term

Email Gateway (Aug 19 2022 at 16:13):

From: M A <tesleft@hotmail.com>
Hi
i am a beginner, first time to write primrec from lemma, however
got an error when parse.

lemma map_app [simp]: "map f xs @ map f ys = map f (xs @ ys)"
apply(induct_tac xs)
apply(auto)
done

goal (2 subgoals): 1. map f [] @ map f ys = map f ([] @ ys) 2. ⋀a list. map f list @ map f ys = map f (list @ ys) ⟹ map f (a # list) @ map f ys = map f ((a # list) @ ys)
prepare to edit
primrev
map f [] = []
map f (a # list) @ map f ys = map f ((a # list) @ ys)

final resultprimrec mmap :: "'a => 'a => 'a list => 'a list" where
"mmap f [] = []" |
"mmap f ((mmap f x) # (mmap f xs)) = mmap f (x # xs)"
value "mmap x+1 [1, 2]"

Inner syntax error⌂
Failed to parse term

Regards,
Martin

Last updated: Apr 19 2024 at 12:27 UTC