Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Hiding type class syntax

view this post on Zulip Email Gateway (Aug 22 2022 at 16:21):

From: Simon Wimmer <wimmersimon@gmail.com>
Dear list,

is there a way to hide syntax stemming from type classes?
In particular, I want to remove the syntax for infinity from Extended_Nat.
I tried

no_syntax infinity :: "'a" ("∞") and
no_syntax infinity :: "'a :: infinity" ("∞"),

but to no avail.

Simon

view this post on Zulip Email Gateway (Aug 22 2022 at 16:21):

From: Simon Wimmer <wimmersimon@gmail.com>
Nevermind, no_notation is what I want.

Last updated: Apr 18 2024 at 04:17 UTC