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
  val x = @{term () :: 'a  'a  bool}


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: Aug 15 2022 at 02:13 UTC