Talk:Converting between implicit and explicit parameters
I tried for an hour to come up with a simple example where this trick is required, but I couldn't. (I've used it in much more complicated stuff, though, so it definitely comes up.) Anybody else more clever at minimal examples? — Tom 7 11:47, 10 October 2006 (EDT)
Using abbreviations to convert from explicit to implicit
I frequently use abbreviations to define a shortcut version of a relation omitting those extra parameters. Thus
%abbrev translate-i : of M A -> of M' A -> type = translate-e M A M'.
%abbrev translate-i = translate-e _ _ _.
The advantage of the abbreviation technique is that you don't need to transform things back and forth: you just use whichever form is more convenient. The only place where abbreviations CANNOT be used is in call patterns. Boyland 22:36, 8 January 2010 (EST)