Andromedans / andromeda

A proof assistant for general type theories
http://www.andromeda-prover.org/
Other
297 stars 34 forks source link

Fixing typing annotations on recursive functions #484

Open andrejbauer opened 4 years ago

andrejbauer commented 4 years ago

This issue is a partial response to #482. A recursive function f of type t is annotated as

let rec f x : t = ...

which makes it look as if f x has type t. The easiest fix here so to instead have

let rec (f : t) x = ...

This is what should be implemented instead of the current solutions.

Alrernatives

  1. In case t is of the form t1 -> t2 we could write let rec f (x : t1) : t2 = ..., but not when t is of the form mlforall a , ....

  2. OCaml allows let rec f : t = fun x -> ... but that relies on examining the syntactic form of the right-hand side, which we prefer to avoid.