search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

"Program Fixpoint" incorrectly translated #45

Closed Casteran closed 3 years ago

Casteran commented 3 years ago

Alectryon translates a "Program Fixpoint" definition into just "Fixpoint"

Require Import Coq.Program.Wf. Require Import Coq.Arith.Arith.

Program Fixpoint f (n : nat ) {wf lt n} : nat := match n with | 0 => 0 | _ => f (n / 2) end.

Zimmi48 commented 3 years ago

Great! We are looking forward to a new release.