Re: [isabelle] partial function



On Mi, 2014-01-08 at 15:29 +0200, Roger H. wrote:

> definition f :: "nat ⇀ nat" where
> "f ≡ [1 ↦ 2, 1 ↦ 3, 1 ↦ 2]"
> 

This syntax is just a shortcut for a sequence of function updates,
starting with the empty map. Thus, later updates just overwrite earlier
ones.

--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.