
  0 | module Data.Container.SubTerm
  1 | 
  2 | -- temporary experimentation
  3 | 
  4 | ||| Like Ord, but with a comparison that can fail
  5 | ||| Can be thought of as computing whether a term is a subterm of another term,
  6 | ||| or as computing common prefixes/subpaths in a tree
  7 | public export
  8 | interface Eq a => MOrd a where
  9 |   constructor MkMOrd
 10 |   mcompare : a -> a -> Maybe Ordering
 11 | 
 12 | public export
 13 | Ord a => MOrd a where
 14 |   mcompare x y = Just $ compare x y
 15 | 
 16 | public export
 17 | isSubTerm : MOrd a => a -> a -> Bool
 18 | isSubTerm x y = case mcompare x y of
 19 |   Just LT => True
 20 |   Just EQ => True
 21 |   _ => False
 22 | 
 23 | -- ||| Should generally be possible to derive with metaprogramming
 24 | -- ||| This sounds like something that should be generally possible to derive
 25 | -- ||| with metaprogramming for any inductive type?
 26 | -- ||| I could imagine this being a built in functionality in a functional language