## Stream: new members

### Topic: example variables

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

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

#### Johan Commelin (Jun 02 2020 at 22:00):

include Y Z f

#### Johan Commelin (Jun 02 2020 at 22:00):

Before the example

#### Bhavik Mehta (Jun 02 2020 at 22:01):

Perfect, thanks!

Last updated: May 10 2021 at 19:16 UTC