Talk:Converting between implicit and explicit parameters

From The Twelf Project

[edit] Annotation example

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)

[edit] 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'.

Or even

%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)