Stream: General

Topic: Obtaining properly localised terms

view this post on Zulip Lukas Stevens (Jul 28 2020 at 09:41):

I have the following situation:

context order begin
ML ‹
  val x = @{term ‹(≤) :: 'a ⇒ 'a ⇒ bool›}
›
end
ML ‹
  x
›

Inside the context I can use x to identify terms that contain the operator ≤ of the type class order. Outside this does not work anymore since x just refers to some free variable called less_eq. How can I get around that?

Last updated: Oct 05 2026 at 04:40 UTC