first_order.language.sum

Stream: maths

[Xin Huajian]

@Floris van Doorn @Jesse Michael Han Hi! I'm trying defining the Godel number of arithmatic language, where there are two binary function in that language. Therefore I tried '''first_order.language.sum''' to define '''.functions 2''' as a disjoint sum of addition and multiplication. Then how should I distinguish them when when defining different operation on addition and multiplication?