Re: [isabelle] Behaviour of Variable.variant_fixes



> The results for x and x' are somewhat unexpected to me:
> 
>   val x = ["x"]: string list
>   val x' = ["x"]: string list
> 
> I expected them to be different. Indeed, they are different when I move
> the BNF definition to the front, before the calls to `variant_fixes`.

One more thing: this doesn't happen for other kinds of operations, e.g.
`Function.add_function`. Executing

  val fun_config = Function_Common.FunctionConfig
    {sequential=true, default=NONE, domintros=false, partials=false}
  fun pat_completeness_auto ctxt =
    Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac ctxt

  val (_, lthy) = Function.add_function
    [(@{binding foo}, NONE, NoSyn)]
    ([(Attrib.empty_binding, @{term "Trueprop (foo (Suc r) = r)"})])
    fun_config pat_completeness_auto lthy

between two calls of `variant_fixes` doesn't exhibit this behaviour
(i.e. fixed variables are preserved). That makes me wonder whether it is
some oddity in BNF, or for type definitions in general.




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