val test : Type0
let test = {| additive int |} -> int
module SyntaxTests

open Add
open FStar.Tactics.Typeclasses

val foo (#a:Type) (#[tcresolve ()] _ : additive a) (x y : a) : Tot a
/
prims.fst.checked FStar.Tactics.Typeclasses.fsti.checked FStar.Pervasives.fsti.checked Add.fst.checked
SyntaxTests.fsti
Type0
Add.additive Prims.int
let test =
  
{| additive int |} -> int