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

fix: typecheck issue

Browse source
This commit is contained in:
Simon Cruanes 2022-08-27 23:42:19 -04:00
parent 4c90405391
commit 28ad97d2b7
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smtlib/Typecheck.ml
View file

@ -128,13 +128,13 @@ let t_as_q t =
| _ -> None | _ -> None
*) *)
let is_real = Ty.is_real let is_real t = Ty.is_real (T.ty t)
(* convert [t] to a real term *) (* convert [t] to a real term *)
let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t =
let conv t = let conv t =
match T.view t with match T.view t with
| _ when Ty.is_real (T.ty t) -> t | _ when is_real t -> t
(* FIXME (* FIXME
| T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n)) | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n))
| T.LIA l -> | T.LIA l ->