Idris's with example expressed with case pattern matching

with-case-examples.idr

import Data.Vect

-- earlier in the docs:

-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#case-expressions
--
-- Another way of inspecting intermediate values of simple types is to
-- use a case expression.
my_filter_case : (a -> Bool) -> Vect n a -> (p ** Vect p a)
my_filter_case p [] = ( _ ** [] )
my_filter_case p (x :: xs) =
  case my_filter_case p xs of
    ( _ ** xs' ) => if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

-- later in the docs is another form of pattern matching on
-- intermediate results, using `with`, which as the documentation
-- suggests, is a more powerful construct than `case`, because `with`
-- can pattern match on values that constribute to later knowledge of
-- other values:

-- http://idris.readthedocs.io/en/latest/tutorial/views.html#the-with-rule-matching-intermediate-values
--
-- Very often, we need to match on the result of an intermediate
-- computation. Idris provides a construct for this, the with rule,
-- inspired by views in Epigram [1], which takes account of the fact
-- that matching on a value in a dependently typed language can affect
-- what we know about the forms of other values.


-- however, the example given for `with` can be implemented with the
-- less powerful `case` pattern matching.
my_filter_with : (a -> Bool) -> Vect n a -> (p ** Vect p a)
my_filter_with p [] = ( _ ** [] )
my_filter_with p (x :: xs) with (my_filter_with p xs)
  | ( _ ** xs' ) = if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )

-- Gentle suggestion:
-- the example given for `with` in
--
-- http://idris.readthedocs.io/en/latest/tutorial/views.html#the-with-rule-matching-intermediate-values
--
-- is one that cannot be expressed with `case`.