Email Gateway (Aug 19 2022 at 16:12): Email Gateway (Aug 19 2022 at 16:12):From: M A <tesleft@hotmail.com>
Hi
in quickspec, i find a lemma and then get 2 subgoals, after rewrite subgoals as primrec and value to see how it works.it return failed to parse term, how to write it and parse successfully?
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 editprimrevmap 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: Nov 21 2024 at 12:39 UTC