Type providers must build one of these in an IO computation.
- Provide : (x : a) ->
Provider a
Return a term to be spliced in
- x
the term to be spliced (i.e. the proof)
- Error : (msg : String) ->
Provider a
Report an error to the user and stop compilation
- msg
the error message