# Zulip Chat Archive

## Stream: new members

### Topic: Making a type

#### Iocta (Jun 28 2020 at 00:50):

I want to create a new type that should act exactly like `real`

. I will later add some subtype predicates to it but for now I just want it to behave like `real`

. How do I do that? I tried `def myreal : Type := real`

but afaict that doesn't have `has_mul`

.

#### Shing Tak Lam (Jun 28 2020 at 01:04):

I guess this might be what you want? I think this has all the properties (typeclasses) that `real`

does? But in general you can just use `variables`

and put whatever typeclasses you want the type of have.

```
import algebra.ordered_field
variables (myreal : Type) [discrete_linear_ordered_field myreal]
```

#### Alex J. Best (Jun 28 2020 at 01:05):

I'm not sure exactly what you want to achieve (it would help if you explained a little more what your actual goal is perhaps).

But you can do this:

```
@[derive has_mul]
def myreal := real
```

to add whatever instances you like automatically my transferring them from real, finding a list of all the possible instances on real wouldn't be recommended though.

You could also do

```
@[reducible]
def myreal := real
```

If you are going to make it a subtype of real later why not make it one now, but a trivial condition if you cant yet define the condition you want so that the type behaves like a subtype.

#### Iocta (Jun 28 2020 at 01:10):

(it would help if you explained a little more what your actual goal is perhaps).

Sure. I want to try proving some theorems from elementary probability as an exercise. I figured it would be easier to start by just saying "a probability is a real" and replace the definitions later, than to start from measure theory ... though I could be wrong

#### Iocta (Jun 28 2020 at 01:13):

```
import data.real.basic
import data.nat.basic
import data.complex.exponential
-- XXX For now `ℝ` denotes a probability, and `real` denotes a real.
-- This should be changed to an actual probability type.
def binomial_coefficient (n k : nat) : int :=
(nat.fact n) / ((nat.fact (n - k)) * (nat.fact k))
def binomial_pmf (n: nat) (p : ℝ) (k : nat) : ℝ :=
(binomial_coefficient n k) * (p ^ k) * (1 - p) ^ (n - k)
def Poisson_pmf (lambda: real) (k: nat) : ℝ :=
(lambda ^ k) / ( (nat.fact k) * (real.exp lambda) )
```

I immediately run into `definition 'Poisson_pmf' is noncomputable, it depends on 'real.division_ring'`

, not sure what to do with that.

#### Alex J. Best (Jun 28 2020 at 01:14):

I'd recommend doing what @Shing Tak Lam says then, maybe not starting from discrete_linear_ordered_field but just `has_mul`

or `comm_semiring`

as variables, assumptions on what your type satisfies, then later if you actually construct the type with these properties all the theorems will apply.

#### Alex J. Best (Jun 28 2020 at 01:15):

you can add `noncomputable theory`

at the top of the file (under imports)

#### Iocta (Jun 28 2020 at 02:33):

Is there a positive reals type?

#### Alex J. Best (Jun 28 2020 at 03:19):

There is `nnreal`

for the reals `\ge 0`

Last updated: May 10 2021 at 17:39 UTC