Stream: Beginner Questions

Topic: definition of a constant

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: Apr 26 2024 at 08:19 UTC