Very basic question about coq. How do I define the following two inductive types?
Type 1 containing: o fo, ffo, fffo... k, sk, ssk, sssk... Note that the f here could alternatively be characterized as the natural number index for o.
Type 2 containing the same but now we can also have terms like fsffsk and sfsfso.
If I understand your first type correctly, you can represent it by combining simpler types defined in the Coq standard library:
Definition t1 : Type := nat + nat.
The + operator on types is the disjoint union of two types. The idea is that the element inl n, which is injected on the left of the union, represents the string fff...o, with n occurrences of f, whereas the element inr n, which is injected on the right of the union, represents the string sss...k, with n occurrences of s.
I do not understand the patterns on the second type. Did you really mean to write fsffsk instead of fsfsfsk?
Do you actually need to base type2's definition on type1 ? Because actually just a simple definition :
Inductive type2 : Type :=
| o : type2
| k : type2
| f : type2 -> type2
| s : type2 -> type2
.
And then define examples like :
Definition typeExample : type2 := f (s (f (s (s (f (s (k))))))).
