sync

Stream: general

[Kevin Buzzard]

I've never quite understood the sync error. Is it posible to get a Lean file with precisely one error in, which is sync?

[orlando]

Hum i try :grinning_face_with_smiling_eyes:

import algebra.category.CommRing.basic
import algebra.ring
import tactic
import category_theory.functor_category -- this transitively imports
import algebra.ring
import category_theory.types
universes v u
/--
##  It's the group functor  Idem,
##  e1 × e2 = e1 e2 - (1-e1)(1-e2)
-/
structure Idem( R : Type v) [comm_ring R] :=
(e  : R)
(certif :  e *e = e)

namespace   Idem
section
variables {R : Type v} [comm_ring R]

@[ext]lemma ext : ∀ {g1 g2 : Idem R}, g1.e = g2.e → g1 = g2 := λ g1 g2,  --- it's ok ? just don't use Bracket ?
begin
  intros h1 ,
  cases g1,                                         ---  difficult i have to analyse !
  cases g2,
  congr ; try { assumption },
end

def one  : Idem (R) := {e := 1,  certif := mul_one 1}
instance  : has_one (Idem R) := ⟨one⟩
lemma one_e : (1 : Idem(R)).e = 1 := rfl

def mul_map' : Idem(R) → Idem (R) → Idem(R) := λ g1 g2, begin
{ e := g1.e * g2.e-(1-g1.e) * (1-g2.e),   --- " exact "
  certif := begin
   sorry,
  end},  -- if i put my mousse here i have sync error !   I forget " exact "  !
end

[Kevin Buzzard]

I was hoping to get it as the only error in the Lean Messages window (click on Info View: Display Messages), i.e. have VS Code display 1 error (your code says it has 16 errors in the bottom left hand corner of VS Code)

[orlando]

okay i try to find other exemple :sweat_smile: