## 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