## Stream: Beginner Questions

### Topic: Attach restriction to type

#### Hernán Rajchert (Oct 26 2022 at 13:32):

Is there a way to encode a restriction in a type, similar to what a "smart constructor" would do in Haskell/PureScript?

I would like to define a type like this

``````type_synonym TimeInterval = "POSIXTime × POSIXTime"
``````

A function that may create it

``````fun createTimeInterval :: "POSIXTime ⇒ POSIXTime ⇒ TimeInterval option" where
"createTimeInterval l r = (if l ≤ r then Some (l, r) else None)"
``````

and then to carry this restriction, so that I don't have to add it to every lemma

``````fun validTimeInterval :: "TimeInterval ⇒ bool" where
"validTimeInterval (l, r) = (l ≤ r)"

theorem inInterval_subset:
"validTimeInterval a ⟹ inInterval a b = (tToSet a ⊆ bToSet b)"
``````

I have the feeling that I might achieve this with locales, but not sure if this is the intended use case.

#### Jan van Brügge (Oct 26 2022 at 13:42):

You would do that with a subtype of TimeInterval, using `typedef`:

``````typedef ValidTimeInterval = "{ (x, y)::TimeInterval . x <= y }"
``````

Then you can get the underlying type using the `Rep_ValidTimeInterval` function and the property is in the theorem `Rep_ValidTimeInterval`

#### Hernán Rajchert (Oct 26 2022 at 14:16):

Thanks! Will try it :)

#### Hernán Rajchert (Oct 26 2022 at 17:58):

It worked great in the proofs, now I need to figure out how to export code from it. I'm getting the following error, need to check how to define the code equation

`````` No code equations for Abs_ValidTimeInterval
``````

#### Hernán Rajchert (Oct 26 2022 at 18:21):

Ah, just defining `code_datatype Abs_ValidTimeInterval` did the trick :D

Last updated: Dec 07 2023 at 20:16 UTC