gistfile1.txt

foo : (m : Nat) -> (n : Nat) -> Dec (LT m n)
foo Z Z = No absurd
foo Z (S k) = Yes (LTESucc LTEZero)
foo (S k) Z = No absurd
foo (S k) (S j) = case foo k j of
                    (Yes prf) => Yes (LTESucc prf)
                    (No contra) => No (\(LTESucc r) => contra r)

foo2 : (m : Nat) -> (n : Nat) -> Dec (LT m n)
foo2 m n with (isLTE (S m) n)
  foo2 m n | (Yes prf) = Yes prf
  foo2 m n | (No contra) = No contra

foo3 : (m : Nat) -> (n : Nat) -> Dec (LT m n)
foo3 m n = isLTE (S m) n

decideLT : (m : Nat) -> (n : Nat) -> Dec (LT m n) 
decideLT Z (S k) = Yes (LTESucc LTEZero) 
decideLT (S k) (S j) = (case (decideLT k j) of
                            (Yes prf) => Yes (shift (S k) j prf)
                            (No contra) => No (ltesuccinjective contra)) 
decideLT _ Z = No succNotLTEzero 

foo jx = do
  Just x <- jx
    | Nothing => foo
  bip x
-- ^ fine

foo2 jx = do
  Just x <- jx
    | Nothing => foo *> blah
  bip x
-- ^ problem

foo2 jx = do
  Just x <- jx
    | Nothing => (foo *> blah)
  bip x
-- ^ solution

beb : a -> b -> Something
beb x y with (blah x)
beb x y | foo = ...
-- ^ with requires parens around blah x for some reason