Is there an equivalent (in
Ltac2 @ external closenl : ident list -> int -> constr -> constr := "ltac2" "constr_closenl". (** [closenl [x₁;...;xₙ] k c] abstracts over variables [x₁;...;xₙ] and replaces them with [Rel(k); ...; Rel(k+n-1)] in [c]. If two names are identical, the one of least index is kept. *)
I guess it's called
substn_vars in OCaml
Ah, I guess it's in
Jason Gross has marked this topic as resolved.
Jason Gross has marked this topic as unresolved.
Or, no, hm, it doesn't seem to be there
(I have written this code myself now, but am still interested if it exists already)
Nope, there is basically nothing atm about named variables
Last updated: Jan 30 2023 at 17:03 UTC