Zulip Chat Archive

Stream: new members

Topic: example variables


view this post on Zulip Bhavik Mehta (Jun 02 2020 at 21:58):

I sometimes use example when I want to test things out, including sometimes when I haven't yet figured out the right statement that I want to prove, so I use example : false := ..., then explore what I can get given the variables I have - but some of the variables I've defined aren't in scope. Is there a trick I can use to get them in scope?

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 22:00):

import category_theory.comma

namespace category_theory
open category limits

universes v u
variables (C : Type u) [category.{v} C]

variables {J : Type v} [small_category J] [has_colimits_of_shape J C]
variables {Y Z : C} (f : Y  Z)

example (K : J  C) : false :=
begin

end

for example I want to use Y, Z and f in this example

view this post on Zulip Johan Commelin (Jun 02 2020 at 22:00):

include Y Z f

view this post on Zulip Johan Commelin (Jun 02 2020 at 22:00):

Before the example

view this post on Zulip Bhavik Mehta (Jun 02 2020 at 22:01):

Perfect, thanks!


Last updated: May 10 2021 at 19:16 UTC