Currently there is a some gnarliness in Nominal LCF and its use, which stems from the fact that several of its operations are in "tactic"-land, but really should be in "multitactic"-land. An example is recursion...
I think that every primitive of Nominal LCF should be considered a multitactic, and then separately these can be converted into tactics by precomposition with the unit. This approach should simplify a number of things, and will clear away some of the gnarliness.
Currently there is a some gnarliness in Nominal LCF and its use, which stems from the fact that several of its operations are in "tactic"-land, but really should be in "multitactic"-land. An example is recursion...
I think that every primitive of Nominal LCF should be considered a multitactic, and then separately these can be converted into tactics by precomposition with the unit. This approach should simplify a number of things, and will clear away some of the gnarliness.