With some help from @nikswamy , I am trying to write mutually recursive functions with decreases clauses.

Consider the following example: variable-arity trees with a label on each edge.

module L = FStar.List.Tot
noeq type tree =
| Leaf
| Node:
  (labels: list nat) -> // I should probably add a `L.noRepeats` refinement here, but this is irrelevant here
  (children: ((x: nat {x 

I'm using Ubuntu linux with a recent FStar and kreMLin from master.
When attempting to run: krml -verbose Introduction.fst -no-prefix Introduction -o test.exe && ./test.exe
Where Introduction is the example from the kreMLin tutorial. I get this long error:

Each asserts should have further detailed docs. These docs should at minimum include:

• Description
• Parameter list with expected data types and description for each parameter.
• Example

This application uses Windows API by including inbuilt windows.h in C to use Beep() function. We can:

1. Devise a way to incorporate Windows API in non-Windows OS so that Beep() function can be accessed by C compiler in those OSes.
   Or...
2. Use an alternative/equivalent function for Beep() - a function which intakes frequency value & time value to produce a sound beep.

Please add