CODEWITHSUNDEEP
isabelle
user1868607
user1868607

Reputation: 2610

Express a parametric abbreviation in Isabelle

I want to abreviate the equivalence class of a point:

r `` {p}

to

[p]

What is the right way to this in Isabelle?

Upvotes: 1

Views: 55

Answers (1)

Manuel Eberl
Manuel Eberl

Reputation: 8298

You can only do this in a context where r is fixed, e.g. an anonymous context or a locale:

context
  fixes r :: "('a × 'a) set"
begin

abbreviation foo ("⟨_⟩" 1000) where
  "⟨p⟩ ≡ r `` {p}"

I used chevrons instead of brackets here because brackets would clash with the syntax for lists, so it wou

Upvotes: 2

Related Questions