# Zulip Chat Archive

## Stream: new members

### Topic: module parameters

#### Thorsten Altenkirch (Nov 01 2020 at 13:46):

Is there anything like module parameters (or section parameters) in Lean? I want to assume that a relation is a decidable partial order without prefixing even construction with this assumption. While I can use `variables`

to abstract over the relation this obviously doesn't work for the properties. because they show only up in the proofs.

#### Mario Carneiro (Nov 01 2020 at 13:51):

this obviously doesn't work for the properties

But it does work for properties

#### Mario Carneiro (Nov 01 2020 at 13:51):

in particular, for typeclass assumptions you can have `variables (R : A -> A -> Prop) [decidable_rel R]`

and it will work as you expect

#### Mario Carneiro (Nov 01 2020 at 13:53):

For other kinds of hypotheses, that are not typeclasses like `variables (R : A -> A -> Prop) (hr : \all x, R x x)`

, you may have to use `include hr`

to include the assumption even in definitions that don't require it (although this may cause a linting warning since it's an unused argument)

#### Thorsten Altenkirch (Nov 01 2020 at 13:54):

Thank you. So where do I say "include hr" when I want to use it in a proof?

#### Mario Carneiro (Nov 01 2020 at 13:57):

```
section
variables (R : A -> A -> Prop) (hr : \all x, R x x)
theorem uses_hr : \all x, R x x := hr
theorem doesnt_use_hr : true := by have := hr -- fail
include hr
theorem uses_hr : true := by have := hr; trivial
end
```

#### Mario Carneiro (Nov 01 2020 at 13:57):

`include`

is scoped like `variable`

#### Mario Carneiro (Nov 01 2020 at 13:57):

you can also undo `include`

using `omit`

Last updated: May 13 2021 at 20:13 UTC