I have defined the reflexive transitive closure of a binary relation. It is "trc R"
I would like to define the trc of a concrete relation. Which definition command should I use? I tried "define" and "definition" to no avail in a locale body. The right hand side would be
= trc myRel
I also tried "value"
locale myloc
begin
definition myRel' where
"myRel' = trc myRel"
should work, but I might be missing something in your question…
And what is the error you are receiving?
Note that HOL already defines a reflexive transitive closure as rtrancl
or rtranclp
.
@Mathias Fleury
Outer syntax error⌂: command expected,
but keyword =⌂ was found
But I realised from your answer that I should use double quotes in the "where" clause. I should train my mind to always use double quotes in concrete syntax.
Last updated: Oct 12 2024 at 20:18 UTC