@@ -486,6 +486,7 @@ data Binder b = Lam { binderTy :: b {-^ type annotation for bound variable-}}
486486 | Guess { binderTy :: b,
487487 binderVal :: b }
488488 | PVar { binderTy :: b }
489+ -- ^ A pattern variable
489490 | PVTy { binderTy :: b }
490491 deriving (Show, Eq, Ord, Functor)
491492{-!
@@ -1082,6 +1083,8 @@ weakenEnv env = wk (length env - 1) env
10821083weakenTmEnv :: Int -> EnvTT n -> EnvTT n
10831084weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))
10841085
1086+-- | Gather up all the outer 'PVar's and 'Hole's in an expression and reintroduce
1087+-- them in a canonical order
10851088orderPats :: Term -> Term
10861089orderPats tm = op [] tm
10871090 where