Re: [isabelle] Definition in jEdit
On Mon, 21 May 2012, Abdullah wrote:
I tried to definition the *consts * but it give me error and I do not know
where is it.,,
Const1:: "type => type"
const_def : " Const1 A = Const1 B ==> A = B"
And the error message is
(((Not a meta-equality (==)
The error(s) above occurred in definition "injective_publicKey":
"A = B" ))))
I am not sure what you are trying to do. The above is not a definition,
it is a statement about injectivity of Const1.
You can achieve that as follows:
datatype 'a test = Const1 'a
lemma "Const1 A = Const1 B ==> A = B" by simp
Const1 as datatype constructor is injective, as demonstrated here, and a
bit more according to the meaning of datatype.
Anyway, if you want to make plain definitions, use 'definition' or 'fun'
as described in the Isabelle/Isar reference manual.
This archive was generated by a fusion of
Pipermail (Mailman edition) and