Commit 8c4456cd authored by Nuria Brede's avatar Nuria Brede

Adapt `surprise` and `circular` examples + fix `LTE`.

parent 6afb9c56
......@@ -10,6 +10,8 @@
> import code.idris.Real.Postulates
> import code.idris.Tree.BinTree
> %default total
> %auto_implicits on
> %access public export
......@@ -521,10 +523,12 @@ zero:
>
> aNecessarilyEmptyList = []
> partial
> surprise : (n : Nat) -> n = 0
>
> surprise n = void (headL aNecessarilyEmptyList)
Try to typecheck the file after uncommenting the |partial| flag above --
The Idris type checker realizes that we are trying to fool the system
and that |surprise| cannot be total.
......@@ -532,9 +536,10 @@ The second potential problem is non-termination. A function may cover
all cases, but still fail to terminate. The extreme case is a completely
circular definition
> circular : Void
> circular = circular
> -- circular : Void
> -- circular = circular
Try to typecheck the file after uncommenting the definition of |circular| --
Idris will warn about missing cases and potentially non-terminating
loops in definitions that are required to be |total|.
......@@ -586,9 +591,9 @@ The type of functions from natural numbers to |Bool|.
\subsubsection*{Exercise \ref{exercise4.2}:}
> Optimal : (X -> Y) -> Type
> Optimal p = (x : X) -> (y : Y) -> val x y <= val x (p x)
> Optimal p = (x : X) -> (y : Y) -> val x y `LTE` val x (p x)
What is the type of |<=|?
What is the type of |`LTE`|?
\subsubsection*{Exercise \ref{exercise4.3}:}
......@@ -631,7 +636,7 @@ The expressions are |3 * 2| on the LHS and |6| on the RHS
>
> ={ Refl }=
>
> ( (mapBinTree f . mapBinTree g) (Leaf x) )>
> ( (mapBinTree f . mapBinTree g) (Leaf x) )
> QED
>
> mapBinTreeSpec2step : (l : BinTree a) -> (r : BinTree a) -> (f : b -> c) -> (g : a -> b) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment