kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Первый раз наткнулся на ошибку в ocaml

Причем свежевставленную: в 4.05.0:

В Why3 в core/term.mli:

val t_const : Number.constant -> term

в core/term.ml:

let t_const c ty = mk_term (Tconst c) (Some ty)
...
let t_const c = match c with
| Number.ConstInt _ -> t_const c ty_int
| Number.ConstReal _ -> t_const c ty_real

В результате экспортится первое из определений t_const, причем с типом:

Number.constant -> Ty.ty -> term

Что интересно - на простом примере не воспроизводится
Subscribe
  • Post a new comment

    Error

    default userpic

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 9 comments