Re: [isabelle] Failed to parse term



Hi Martin,

what is your definition of @ ? Did you get it from the Tutorial? As I mentioned it would be better to provide us a working Isabelle theory containing 

theory Blabla
imports main

and all the necessary definitions so we could try it out.

- Gergely

-----Original Message-----
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of M A
Sent: Wednesday, October 29, 2014 12:42 PM
To: isabelle-users at cl.cam.ac.uk
Subject: [isabelle] Failed to parse term


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 		 	   		   		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.