robstewart57 · November 13, 2017 09:27
diff --git a/with-case-examples.idr b/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`.
	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`.