Jason Gross (Aug 28 2022 at 09:54): Jason Gross (Aug 28 2022 at 09:54):Is there a good way to implement liftn for projects that need to stay compatible with Coq 8.15? I'm trying to decide whether to copy over the code in tac2core.ml so that I can stuff https://github.com/coq/coq/pull/16413 in a plugin, or whether I should port the implementation of liftn to Ltac2 (with the corresponding loss of efficiency due to interpretation + not having access to physical equality), or whether, since I really only need to turn x into (fun _ : unit => x), I should do something really kludgy like Std.eval_cbv <beta> in mkApp '(fun y (_ : unit) => y) [|x|] (except I want to preserve beta-redexes in x, so maybe I should turn all applications of lambdas into applications of dummy identifiers to lambdas? But this already almost as painful as reimplementing liftn...)
Is there a better way?
Jason Gross (Aug 28 2022 at 10:25):My current hack: turn x into x : True unsafely, use the standard antiquotation mechanism to get fun (_ : unit) => x : True (since retyping doesn't peek under casts), and then use unsafe constr manipulation to strip off the cast
Jason Gross (Aug 28 2022 at 15:44):Actually, '(fun (_ : unit) => $x) doesn't do de Bruijn lifting, so my new hack is '(match $x return unit -> True with v => fun _ : unit => v end)
Last updated: Oct 08 2024 at 15:02 UTC