example variables

Stream: new members

[Bhavik Mehta]

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]

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]

include Y Z f

[Johan Commelin]

Before the example

[Bhavik Mehta]

Perfect, thanks!