Zulip Chat Archive

Stream: new members

Topic: module parameters


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 01 2020 at 13:51):

this obviously doesn't work for the properties

But it does work for properties

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 01 2020 at 13:57):

include is scoped like variable

view this post on Zulip Mario Carneiro (Nov 01 2020 at 13:57):

you can also undo include using omit


Last updated: May 13 2021 at 20:13 UTC