TypeDD-Samples icon indicating copy to clipboard operation
TypeDD-Samples copied to clipboard

How does the inferring work on this line?

Open coodoo opened this issue 6 years ago • 0 comments

https://github.com/edwinb/TypeDD-Samples/blob/a5c08a13e6a6ec804171526aca10aae946588323/Chapter6/Printf.idr#L27

Use an underscore (_) for the format, because Idris can infer from the type that it must be toFormat (unpack fmt).

This's the explanation from the book for above line but I'm still a bit puzzled by how does the inferring work here? Since fmt comes in as a String type, how does it become a Format type when passed to printfFmt?

coodoo avatar Jan 22 '19 08:01 coodoo