fact: Definition autoinduct {A} (a : A) : TemplateMonad typed_term := a' <- tmEval cbv a ;; t <- tmQuote a' ;; let (hd, args) := decompose_app t in match hd with | tFix mfix idx => match nth_error mfix idx with | Some f => match nth_error args (f.(rarg)) with | Some x => tmUnquote x | None => tmFail "not enough arguments for induction" end | None => tmFail "ill-typed fixpoint" end | _ => tmFail "passed term does not unfold to a fixpoint" end.
imports: MetaCoq.Template(All) MetaCoq.Utils(bytestring) List