Explain how to what is a reflection tactic and how to write one using Ltac2. Take inspiration from https://github.com/rocq-community/metaprogramming-rosetta-stone/blob/main/real_simplifier/ltac2_reflexive/theories/RealSimpl.v or maybe sth simpler ?
Explain how to what is a reflection tactic and how to write one using Ltac2.
Take inspiration from https://github.com/rocq-community/metaprogramming-rosetta-stone/blob/main/real_simplifier/ltac2_reflexive/theories/RealSimpl.v or maybe sth simpler ?