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 type of is_a

Browse source
This commit is contained in:
Simon Cruanes 2022-08-12 23:21:56 -04:00
parent 85eef2d117
commit 85314379a5
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/base/Data_ty.ml
View file

@ -115,7 +115,6 @@ let cstor tst c : Term.t =
List.map (fun s -> Lazy.force s.select_ty) (Lazy.force c.cstor_args) List.map (fun s -> Lazy.force s.select_ty) (Lazy.force c.cstor_args)
in in
let ty = Term.arrow_l tst ty_args ty_ret in let ty = Term.arrow_l tst ty_args ty_ret in
Log.debugf 50 (fun k -> k "cstor %a (ty %a)" Cstor.pp c Term.pp ty);
Term.const tst @@ Const.make (Cstor c) ops ~ty Term.const tst @@ Const.make (Cstor c) ops ~ty
let select tst s : Term.t = let select tst s : Term.t =
@ -125,7 +124,9 @@ let select tst s : Term.t =
Term.const tst @@ Const.make (Select s) ops ~ty Term.const tst @@ Const.make (Select s) ops ~ty
let is_a tst c : Term.t = let is_a tst c : Term.t =
Term.const tst @@ Const.make (Is_a c) ops ~ty:(Term.bool tst) let ty_arg = Lazy.force c.cstor_ty in
let ty = Term.arrow tst ty_arg (Term.bool tst) in
Term.const tst @@ Const.make (Is_a c) ops ~ty
let as_data t = let as_data t =
match Term.view t with match Term.view t with