fact: Fixpoint locate (e:E) (t:tree) (c:context) : context + E * location := match t with | Null_t => inl c | Two_t tl em tr => match comp e em with | Lt => locate e tl $ TwoLeftHole_c em tr c | Eq => inr (em, TwoHole_l tl tr c) | Gt => locate e tr $ TwoRightHole_c tl em c end | Three_t tl el tm er tr => match comp e el, comp e er with | Lt, _ => locate e tl $ ThreeLeftHole_c el tm er tr c | Eq, _ => inr (el, ThreeLeftHole_l tl tm er tr c) | Gt, Lt => locate e tm $ ThreeMiddleHole_c tl el er tr c | _, Eq => inr (er, ThreeRightHole_l tl el tm tr c) | _, Gt => locate e tr $ ThreeRightHole_c tl el tm er c end end.
imports: ExtLib.Structures.Monads ExtLib.Data.Monads.OptionMonad ExtLib.Programming.Extras