src/Doc/ProgProve/Types_and_funs.thy
 changeset 51393 df0f306f030f parent 48985 5386df44a037 child 51465 c5c466706549
equal inserted replaced
51392:635562bc14ef 51393:df0f306f030f
`    89 "lookup [] x = None" |`
`    89 "lookup [] x = None" |`
`    90 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"`
`    90 "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"`
`    91 `
`    91 `
`    92 text{*`
`    92 text{*`
`    93 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.`
`    93 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.`
`       `
`    94 Pairs can be taken apart either by pattern matching (as above) or with the`
`       `
`    95 projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}`
`       `
`    96 abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates`
`       `
`    97 @{text "\<tau>\<^isub>1 \<times> (\<tau>\<^isub>2 \<times> \<tau>\<^isub>3)"}.`
`    94 `
`    98 `
`    95 \subsection{Definitions}`
`    99 \subsection{Definitions}`
`    96 `
`   100 `
`    97 Non recursive functions can be defined as in the following example:`
`   101 Non recursive functions can be defined as in the following example:`
`    98 *}`
`   102 *}`