simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

handle :named attribute in smtlib

Browse source
This commit is contained in:
Simon Cruanes 2020-08-18 10:01:36 -04:00
parent c5180f3f63
commit 7d399ba201
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smtlib/Typecheck.ml
View file

@ -287,6 +287,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
ill_typed ctx "term `%a`@ should have type `%a`" T.pp t Ty.pp ty_expect
);
t
| PA.Attr (t, [":named",_]) -> conv_term ctx t
| _ ->
errorf_ctx ctx "unsupported term %a" PA.pp_term t