lifting for primitive definitions;
explicit conversions from and to lists of coefficients, used for generated code;
replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions;
prefer pre-existing gcd operation for gcd
(* Author: Andreas Lochbihler, KIT *)
header {* Pretty syntax for almost everywhere constant functions *}
theory FinFun_Syntax
imports FinFun
begin
type_notation
finfun ("(_ =>f /_)" [22, 21] 21)
type_notation (xsymbols)
finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
notation
finfun_const ("K$/ _" [0] 1) and
finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
finfun_apply (infixl "$" 999) and
finfun_comp (infixr "o$" 55) and
finfun_comp2 (infixr "$o" 55) and
finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
notation (xsymbols)
finfun_comp (infixr "\<circ>$" 55) and
finfun_comp2 (infixr "$\<circ>" 55)
end