9c8f57f322
@Kha Not sure whether we should have an option for supressing this information or not. We need this information for diagnosing problems. For example, I was trying to understand why the elaborator was looping. I suspected it was the TC module, but I was not getting any trace messages since the symbol was overloaded, and the case that did not work was the expensive one :(
15 lines
619 B
Text
15 lines
619 B
Text
[Meta.synthInstance] HasAdd String ==> HasAdd String
|
||
[Meta.synthInstance]
|
||
[Meta.synthInstance] main goal HasAdd String
|
||
[Meta.synthInstance.newSubgoal] HasAdd String
|
||
[Meta.synthInstance.globalInstances] HasAdd String #[]
|
||
[Meta.synthInstance] remaining fuel 999
|
||
[Meta.synthInstance] failed
|
||
foo "hello" : String × String
|
||
[Meta.synthInstance] HasAdd Bool ==> HasAdd Bool
|
||
[Meta.synthInstance]
|
||
[Meta.synthInstance] main goal HasAdd Bool
|
||
[Meta.synthInstance.newSubgoal] HasAdd Bool
|
||
[Meta.synthInstance.globalInstances] HasAdd Bool #[]
|
||
[Meta.synthInstance] remaining fuel 999
|
||
[Meta.synthInstance] failed
|