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