Gergely Buday (Aug 25 2020 at 13:32): Gergely Buday (Aug 25 2020 at 13:32):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"
Mathias Fleury (Aug 25 2020 at 13:39):locale myloc
begin
definition myRel' where
"myRel' = trc myRel"
should work, but I might be missing something in your question…
Mathias Fleury (Aug 25 2020 at 13:40):And what is the error you are receiving?
Manuel Eberl (Aug 25 2020 at 13:40):Note that HOL already defines a reflexive transitive closure as rtrancl or rtranclp.
Gergely Buday (Aug 25 2020 at 13:44):@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: Dec 21 2024 at 12:33 UTC