# Computable Acc.rec and WellFounded.fix #

This file exports no public definitions / theorems, but by importing it the compiler will
be able to compile `Acc.rec`

and functions that use it. For example:

Before:

```
-- failed to compile definition, consider marking it as 'noncomputable'
-- because it depends on 'WellFounded.fix', and it does not have executable code
def log2p1 : Nat → Nat :=
WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
let m := n / 2
if h : m < n then
IH m h + 1
else
0
```

After:

```
import Std.WF
def log2p1 : Nat → Nat := -- works!
WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
let m := n / 2
if h : m < n then
IH m h + 1
else
0
#eval log2p1 4 -- 3
```