Stream: Coq users

Topic: Type Annotation - Extraction to Ocaml


view this post on Zulip Aishwarya (Feb 21 2021 at 03:42):

Is it possible to instruct the extraction to ML to include type annotations in function signatures?

For instance, instead of producing this:

(** val foo : int -> int **)
let foo n = n + 1
I would like the following:
let foo (n:int) : int = n


Last updated: Feb 01 2023 at 11:04 UTC