fact: Definition fail_strs (l : mlist dyn) : M.t string := fix2 (fun _ _ => string) (fun go l (acc : mlist string) => match l with | [m: ] => let r := reduce (RedVmCompute) (string_rev (string_rev_flatten acc)) in M.ret r | D :m: l => mmatch D with | [? s] @Dyn string s => go l (s :m: acc) | _ => dcase D as t in s <- M.pretty_print t; go l (s :m: acc) end end) l [m:].
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)