...

Figure 19: Examples of docstrings generated, on a few selected tasks from the CodeXGLUE benchmark. The
highlighted yellow portion is the generated docstring, the lines above and below are given as context to the
model. The last example shows how the model handles long sets of parameters. We use “...” for code we
removed for the sake of presentation, to keep the example brief.

46

/-- A q u a s i - p r e f u n c t o i d i s 1- c o n n e c t e d i f f a l l i t s e t a l i s a t i o n s a r e 1- c o n n e c t e d . -/
theorem connected_iff_etalisation [C D : precategoroid] (P : quasi_prefunctoid C D) :

π1P = 0 ↔ ∀f : C → D, π1(P ⟨f⟩)) = 0 :=

begin

split,
{ intros h f,

rw pi_1_etalisation at h,
simp [h],
refl

},
{ intro h,

have := @quasi_adjoint C D P,
simp [←pi_1_etalisation, this, h],
refl

}
end
CodeLlama2