Re: [isabelle] File.use function

because they are
statically fixed bindings to immutable values.


Maybe you were actually
thinking about assignable references.

Yes I didn't tought of that but that's what I want to do : modify the value of variables inside my code. Yet using references with this following code fails :
val proof_congr = ref []
val proof_inst  = ref []

val _ = use proof_hints_fn

proof_hints_fn containing :
 proof_inst := X;
 proof_congr := Y

When executing, it now says that 'proof_inst' and 'proof_congr' are not declared. I guess that when calling use, the context of the call isn't inherited. But this is bizarre since it works inside an interactive session...


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.