summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Sat, 08 Jul 2017 19:03:42 +0200 | |

changeset 69841 | d2283b15d2ca |

parent 69840 | 0c9bba1e8e97 |

child 69842 | 985eb3b647ab |

.

--- a/Exercises/ex12/ex12.thy Fri Jul 07 21:00:57 2017 +0200 +++ b/Exercises/ex12/ex12.thy Sat Jul 08 19:03:42 2017 +0200 @@ -24,6 +24,9 @@ fun deq :: "'a queue \<Rightarrow> 'a queue" where "deq (xs,ys) = balance (xs, tl ys)" +text \<open>Note that we assume that the size computation in \<open>balance\<close> only takes constant time. +In reality the time is linear. How would you avoid that?\<close> + fun t_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where "t_enq a (xs,ys) = 1 + (if size xs + 1 \<le> size ys then 0 else size xs + 1 + size ys)"