fact: Definition open_pattern {A} {m} {T : forall x, MTele_Ty (m x)} {y : A} {a : ArgsOf (m y)} : forall(p : pattern A (fun x => MFA (T x))), M (apply_sort (T y) a) := Eval lazy beta iota match zeta delta [meq_sym] in fix go p := match p return M _ with | pany f => apply_C Propₛ (f y) a | pbase x f u => oeq <- M.unify x y u; match oeq return M (apply_sort (T y) a) with | mSome eq => match eq in meq _ z return forall a : ArgsOf (m z), M (apply_sort (T z) a) with | meq_refl => apply_C Propₛ f end a | mNone => M.raise DoesNotMatch end | ptele f => c <- M.evar _; go (f c) | psort f => M.mtry' (go (f Propₛ)) (fun e => oeq <- M.unify e DoesNotMatch UniMatchNoRed; match oeq with | mSome _ => go (f Typeₛ) | mNone => M.raise e end ) end .
imports: Mtac2(Base Logic Datatypes List MTele)