# Re: [isabelle] Fwd: Code generation for typedefs with an invariant

Small addition: another application of this is to make a "safe" constructor for types with invariants that returns "None" if the given value does not fulfil the invariant, e.g.:
```
mk_pos_nat :: nat ⇒ good_nat option
mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None)

```
One can do this with an auxiliary function that returns a default value instead of None, but then you have to check the condition twice.
```
```
The best possible solution I see here is if "code abstype" could handle not only equations of the form "projection (fun_with_invariant x y z) = …" but relations involving "canonical" relators on types. In the above case, one would then not have a code equation but a code relation:
```
rel_fun (=) (rel_option pcr_good_nat)
(λn. if good n then Some n else None) mk_good_nat

Similarly, the function in my last email have the following relations:

rel_fun (=) (list_all2 pcr_good_nat)
my_complicated_computation my_complicated_computation'

The actual generated code should of course be:

mk_pos_nat n = (if good_nat n then Some (Abs_good_nat n) else None

```
my_complicated_computation' xs = map Abs_good_nat (my_complicated_computation xs)
```
```
Which is exactly the m_complicated_computation' that comes out of the lift_definition anyway (and I imagine there's a one-to-one correspondence between the map operations in the def lemma and the relators in the transfer lemma).
```

```
So, not sure – is there some fundamental problem with implementation something like this in the code generator?
```
Manuel

On 14/10/2021 21:31, Manuel Eberl wrote:
```
```Hello,

I have a typedef of the form

typedef good_nat = "{n::nat. good n}"

```
and I have an executable function that produces a "nat list" where I have proven that all entries are good.
```
```
How can I lift that to an *executable* function that produces a "good_nat list" instead?
```
```
The way I see it, the usual approach of doing a "code abstype" and specifying the code equation in terms of some projection out of the "type with invariant" to "type without invariant" doesn't work here because I have lists of these things.
```
```
I do have a workaround involving a second typedef for intermediate results, but it is very boilerplatey and I'd be happy to know if there is something easier.
```
See attachment for all the details.

Thanks,

Manuel
```
```

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.