Lines Matching refs:function
146 \isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the
171 primitive recursive function definitions.
175 comes equipped with a \isa{size} function from $t$ into the natural numbers
270 \isacommand{primrec} function definition is turned into a proper
288 datatypes, including those involving function spaces, are covered in
291 form of recursive function definition that goes well beyond
388 involving function spaces is permitted: the recursive type may occur on the
389 right of a function arrow, but never on the left. Hence the above can of worms
397 If you need nested recursion on the left of a function arrow, there are
422 update function, and prove that they behave as expected.
478 termination automatically. More advanced function definitions, including user
480 in a separate tutorial~\cite{isabelle-function}.