Email Gateway (Aug 18 2022 at 19:50): Email Gateway (Aug 18 2022 at 19:50):From: Abdullah <mr.ab15@gmail.com>
Dear All
I tried to definition the *consts * but it give me error and I do not know
where is it.,,
consts
Const1:: "type => type"
defs
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" ))))
Best Regards,
Email Gateway (Aug 18 2022 at 19:51):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC