-*- coding: utf-8; -*- ;; Note: (buffer-size) is 4447 Debugger entered: nil (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil)) (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))) (let* ((type (or (flymake-diagnostic-type diagnostic) :error)) (beg (let* ((cl-x diagnostic)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 2)))) (end (let* ((cl-x diagnostic)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 3)))) (convert #'(lambda (cell) (flymake-diag-region (current-buffer) (car cell) (cdr cell)))) ov) (cond ((and (consp beg) (not (null end))) (setq beg (car (funcall convert beg))) (if (consp end) (progn (setq end (car (funcall convert end)))))) ((consp beg) (let* ((b (funcall convert beg)) (a (if b (car-safe ...) (signal ... ...)))) (progn (setq beg a) (setq end b))))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 beg))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 end)))) (let* ((--cl-var-- (flymake-diagnostics beg end)) (e nil) (eov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq e (car --cl-var--)) (setq eov (let* ((cl-x e)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 9)))) (if (flymake--equal-diagnostic-p e diagnostic) (progn (if foreign (progn (debug) (throw ... nil)) (progn (let* ... ... ...) (let* ... ... ...)) (flymake--delete-overlay eov)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq ov (make-overlay beg end)) (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 (overlay-start ov)))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 (overlay-end ov))))) (overlay-put ov 'category (flymake--lookup-type-property type 'flymake-category)) (let* ((--cl-var-- (append (reverse (let* (...) (progn ... ...))) (reverse (flymake--lookup-type-property type 'flymake-overlay-control)) (alist-get type flymake-diagnostic-types-alist))) (value nil) (ov-prop nil)) (while (consp --cl-var--) (progn (setq value (car --cl-var--)) (setq ov-prop (car-safe (prog1 value (setq value ...))))) (overlay-put ov ov-prop value) (setq --cl-var-- (cdr --cl-var--))) nil) (let* ((--cl-default-maybe-- #'(lambda (prop value) (if (plist-member ... prop) nil (overlay-put ov prop ...))))) (progn (funcall --cl-default-maybe-- 'face 'flymake-error) (funcall --cl-default-maybe-- 'before-string (flymake--fringe-overlay-spec (flymake--lookup-type-property type 'flymake-bitmap (alist-get 'bitmap (alist-get type flymake-diagnostic-types-alist))))) (funcall --cl-default-maybe-- 'help-echo #'(lambda (window _ov pos) (let (...) (save-current-buffer ...)))) (funcall --cl-default-maybe-- 'severity (warning-numeric-level :error)) (funcall --cl-default-maybe-- 'priority (cons nil (+ 40 (overlay-get ov 'severity)))))) (overlay-put ov 'evaporate t) (overlay-put ov 'flymake-overlay t) (overlay-put ov 'flymake-diagnostic diagnostic) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq (type-of cl-x) cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 9 ov))) (if flymake-show-diagnostics-at-end-of-line (progn (save-excursion (goto-char (overlay-start ov)) (let* ((start (line-end-position)) (end (min ... ...)) (eolov (car ...))) (if eolov (let* (...) (overlay-put v ... ...)) (setq eolov (make-overlay start end nil t nil)) (overlay-put eolov 'flymake-overlay t) (overlay-put eolov 'flymake--eol-overlay t) (overlay-put eolov 'flymake-eol-source-overlays (list ov)) (overlay-put eolov 'evaporate (not ...))) (overlay-put ov 'eol-ov eolov))))) (if ov nil (debug)) ov) (catch '--cl-block-flymake--highlight-line-- (let* ((type (or (flymake-diagnostic-type diagnostic) :error)) (beg (let* ((cl-x diagnostic)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 2)))) (end (let* ((cl-x diagnostic)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3)))) (convert #'(lambda (cell) (flymake-diag-region (current-buffer) (car cell) (cdr cell)))) ov) (cond ((and (consp beg) (not (null end))) (setq beg (car (funcall convert beg))) (if (consp end) (progn (setq end (car ...))))) ((consp beg) (let* ((b (funcall convert beg)) (a (if b ... ...))) (progn (setq beg a) (setq end b))))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 beg))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 end)))) (let* ((--cl-var-- (flymake-diagnostics beg end)) (e nil) (eov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq e (car --cl-var--)) (setq eov (let* ((cl-x e)) (progn (or ... ...) (aref cl-x 9)))) (if (flymake--equal-diagnostic-p e diagnostic) (progn (if foreign (progn ... ...) (progn ... ...) (flymake--delete-overlay eov)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq ov (make-overlay beg end)) (if (= (overlay-start ov) (overlay-end ov)) (progn (delete-overlay ov) (debug) (throw '--cl-block-flymake--highlight-line-- nil))) (progn (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 2 (overlay-start ov)))) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 3 (overlay-end ov))))) (overlay-put ov 'category (flymake--lookup-type-property type 'flymake-category)) (let* ((--cl-var-- (append (reverse (let* ... ...)) (reverse (flymake--lookup-type-property type ...)) (alist-get type flymake-diagnostic-types-alist))) (value nil) (ov-prop nil)) (while (consp --cl-var--) (progn (setq value (car --cl-var--)) (setq ov-prop (car-safe (prog1 value ...)))) (overlay-put ov ov-prop value) (setq --cl-var-- (cdr --cl-var--))) nil) (let* ((--cl-default-maybe-- #'(lambda (prop value) (if ... nil ...)))) (progn (funcall --cl-default-maybe-- 'face 'flymake-error) (funcall --cl-default-maybe-- 'before-string (flymake--fringe-overlay-spec (flymake--lookup-type-property type 'flymake-bitmap (alist-get ... ...)))) (funcall --cl-default-maybe-- 'help-echo #'(lambda (window _ov pos) (let ... ...))) (funcall --cl-default-maybe-- 'severity (warning-numeric-level :error)) (funcall --cl-default-maybe-- 'priority (cons nil (+ 40 (overlay-get ov ...)))))) (overlay-put ov 'evaporate t) (overlay-put ov 'flymake-overlay t) (overlay-put ov 'flymake-diagnostic diagnostic) (let* ((cl-x diagnostic)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--diag-tags) t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (let* ((v cl-x)) (aset v 9 ov))) (if flymake-show-diagnostics-at-end-of-line (progn (save-excursion (goto-char (overlay-start ov)) (let* ((start ...) (end ...) (eolov ...)) (if eolov (let* ... ...) (setq eolov ...) (overlay-put eolov ... t) (overlay-put eolov ... t) (overlay-put eolov ... ...) (overlay-put eolov ... ...)) (overlay-put ov 'eol-ov eolov))))) (if ov nil (debug)) ov)) flymake--highlight-line(#s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 (cons d (aref v 4))))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode (progn (flymake--highlight-line d ...))) (let* ((cl-x d)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 1 ...)))))) (progn (or (stringp (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (cl--assertion-failed '(stringp (flymake--diag-locus d)))) nil) (let* ((v (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (v (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 5))))) (puthash v (cons d (gethash v v)) v)))) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--diag cl-x))) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 (cons d (aref v 4))))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode (progn ...)) (let* (...) (or ... ...) (let* ... ...))))) (progn (or (stringp (let* (...) (progn ... ...))) (cl--assertion-failed '(stringp ...))) nil) (let* ((v (let* (...) (progn ... ...))) (v (let* (...) (progn ... ...)))) (puthash v (cons d (gethash v v)) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 (cons d ...)))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus (find-buffer-visiting locus))) (progn (save-current-buffer (set-buffer locus) (if flymake-mode ...) (let* ... ... ...)))) (progn (or (stringp (let* ... ...)) (cl--assertion-failed '...)) nil) (let* ((v (let* ... ...)) (v (let* ... ...))) (puthash v (cons d (gethash v v)) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (save-restriction (widen) (cond (region (let* ((--cl-var-- (let* (...) (progn ... ...))) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* (...) (progn ... ...))) (if (or (not ...) (flymake--intersects-p ... ... ... ...)) (progn (flymake--delete-overlay ov)) (setq surviving (nconc surviving ...))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 surviving))) nil)) ((not (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 2)))) (let* ((--cl-var-- (let* (...) (progn ... ...))) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* (...) (progn ... ...))) (if ov (progn (flymake--delete-overlay ov))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 ...))) (flymake--highlight-line d)) (t (if (or (buffer-live-p locus) (setq locus ...)) (progn (save-current-buffer ... ... ...))) (progn (or (stringp ...) (cl--assertion-failed ...)) nil) (let* ((v ...) (v ...)) (puthash v (cons d ...) v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil)) (progn (let ((tail diags)) (while tail (let ((d (car tail))) (let* ((cl-x d)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 6 backend))) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* ((--cl-var-- (let* ... ...)) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* ... ...)) (if (or ... ...) (progn ...) (setq surviving ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 surviving))) nil)) ((not (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 2)))) (let* ((--cl-var-- (let* ... ...)) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag (car --cl-var--)) (setq ov (let* ... ...)) (if ov (progn ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (let* ((v cl-x)) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ((cl-x d)) (progn (or ... ...) (aref cl-x 1)))) (cond ((eq locus (current-buffer)) (let* (...) (or ... ...) (let* ... ...)) (flymake--highlight-line d)) (t (if (or ... ...) (progn ...)) (progn (or ... ...) nil) (let* (... ...) (puthash v ... v)))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil))) (progn (let ((--cl-keys-- --cl-rest--)) (while --cl-keys-- (cond ((memq (car --cl-keys--) '(:backend :state :region :allow-other-keys)) (if (cdr --cl-keys--) nil (error "Missing argument for %s" (car --cl-keys--))) (setq --cl-keys-- (cdr (cdr --cl-keys--)))) ((car (cdr (memq ... --cl-rest--))) (setq --cl-keys-- nil)) (t (error "Keyword argument %s not one of (:backend :state :region)" (car --cl-keys--)))))) (progn (let ((tail diags)) (while tail (let ((d (car tail))) (let* ((cl-x d)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 6 backend))) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* ((--cl-var-- ...) (diag nil) (ov nil) (surviving nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag ...) (setq ov ...) (if ... ... ...) (setq --cl-var-- ...) (setq --cl-var-- nil)) (let* (...) (or ... ...) (let* ... ...)) nil)) ((not (let* (...) (progn ... ...))) (let* ((--cl-var-- ...) (diag nil) (ov nil) (--cl-var-- t)) (while (consp --cl-var--) (setq diag ...) (setq ov ...) (if ov ...) (setq --cl-var-- ...) (setq --cl-var-- nil)) nil) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 4 nil))) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* (...) (progn ... ...))) (cond ((eq locus ...) (let* ... ... ...) (flymake--highlight-line d)) (t (if ... ...) (progn ... nil) (let* ... ...))) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil)))) (let* ((backend (car (cdr (plist-member --cl-rest-- ':backend)))) (state (car (cdr (plist-member --cl-rest-- ':state)))) (region (car (cdr (plist-member --cl-rest-- ':region))))) (progn (let ((--cl-keys-- --cl-rest--)) (while --cl-keys-- (cond ((memq (car --cl-keys--) '...) (if (cdr --cl-keys--) nil (error "Missing argument for %s" ...)) (setq --cl-keys-- (cdr ...))) ((car (cdr ...)) (setq --cl-keys-- nil)) (t (error "Keyword argument %s not one of (:backend :state :region)" (car --cl-keys--)))))) (progn (let ((tail diags)) (while tail (let ((d ...)) (let* (...) (or ... ...) (let* ... ...)) (setq tail (cdr tail))))) (save-restriction (widen) (cond (region (let* (... ... ... ... ...) (while ... ... ... ... ... ...) (let* ... ... ...) nil)) ((not (let* ... ...)) (let* (... ... ... ...) (while ... ... ... ... ... ...) nil) (let* (...) (or ... ...) (let* ... ...)) (flymake--clear-foreign-diags state)) (t)) (let* ((--cl-var-- diags) (d nil) (locus nil) (--cl-var-- t)) (while (consp --cl-var--) (setq d (car --cl-var--)) (setq locus (let* ... ...)) (cond (... ... ...) (t ... ... ...)) (setq --cl-var-- (cdr --cl-var--)) (setq --cl-var-- nil)) nil) (setq flymake--mode-line-counter-cache nil))))) flymake--publish-diagnostics((#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ... :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) :backend eglot-flymake-backend :state #s(flymake--state :running backend-token2723 :reported-p nil :disabled nil :diags (... ... ... ... ... ...) :foreign-diags #) :region (1 . 4448)) (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 1)))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time (time-since flymake-check-start-time))))))) (let ((state (or (gethash backend flymake--state) (error "Can't find state for %s in `flymake--state'" backend))) expected-token) (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* (...) (progn ...)) (signal 'wrong-type-argument (list ... cl-x))) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* ((cl-x state)) (progn (or ... ...) (aref cl-x 1)))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time (time-since flymake-check-start-time))))))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq (type-of cl-x) cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 t))) (if (and flymake-show-diagnostics-at-end-of-line (not (cl-set-difference (flymake-running-backends) (flymake-reporting-backends)))) (progn (flymake--update-eol-overlays))) (flymake--update-diagnostics-listings (current-buffer))) (let* ((explanation (car (cdr (plist-member --cl-rest-- ':explanation)))) (force (car (cdr (plist-member --cl-rest-- ':force)))) (region (car (cdr (plist-member --cl-rest-- ':region))))) (let ((state (or (gethash backend flymake--state) (error "Can't find state for %s in `flymake--state'" backend))) expected-token) (cond ((null state) (flymake-error "Unexpected report from unknown backend %s" backend)) ((let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3))) (flymake-error "Unexpected report from disabled backend %s" backend)) ((progn (setq expected-token (let* (...) (progn ... ...))) (null expected-token)) (flymake-error "Unexpected report from stopped backend %s" backend)) ((not (or (eq expected-token token) force)) (flymake-error "Obsolete report from backend %s with explanation %s" backend explanation)) ((eq :panic report-action) (flymake--disable-backend backend explanation)) ((not (listp report-action)) (flymake--disable-backend backend (format "Unknown action %S" report-action)) (flymake-error "Expected report, but got unknown key %s" report-action)) (t (flymake--publish-diagnostics report-action :backend backend :state state :region region) (if flymake-check-start-time (progn (flymake--log-1 :debug 'flymake "backend %s reported %d diagnostics in %.2f second(s)" backend (length report-action) (float-time ...)))))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and (memq ... cl-struct-flymake--state-tags) t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 t))) (if (and flymake-show-diagnostics-at-end-of-line (not (cl-set-difference (flymake-running-backends) (flymake-reporting-backends)))) (progn (flymake--update-eol-overlays))) (flymake--update-diagnostics-listings (current-buffer)))) flymake--handle-report(eglot-flymake-backend backend-token2723 (#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) :region (1 . 4448)) apply(flymake--handle-report eglot-flymake-backend backend-token2723 ((#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) :region (1 . 4448))) (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args)) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args)))) (closure ((buffer . #) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args)))))((#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start ... :end ...) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) :region (1 . 4448)) funcall((closure ((buffer . #) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply ... backend token args))))) (#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start ... :end ...) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start ... :end ...) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start ... :end ...))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466)) :region (1 . 4448)) (save-restriction (widen) (funcall eglot--current-flymake-report-fn diags :region (cons (point-min) (point-max)))) eglot--report-to-flymake((#s(flymake--diag :locus # :beg 3372 :end 3378 :type eglot-note :text "Lean 4: Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 3 :range (:start (:line 79 :character 0) :end (:line 79 :character 6)) :message "Finset.sum.{u, v} {β : Type u} {α : Type v} [inst✝ : AddCommMonoid β] (s : Finset α) (f : α → β) : β" :fullRange (:start (:line 79 :character 0) :end (:line 79 :character 6)))) :overlay-properties nil :overlay # :orig-beg 3372 :orig-end 3378) #s(flymake--diag :locus # :beg 3588 :end 3591 :type eglot-error :text "Lean 4: unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 86 :character 11) :end (:line 87 :character 0)) :message "unsolved goals\ncase mp.zero\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nt : Fin Nat.zero → V\nht : ↑(blade V t) ≠ 0\nn : Finset (Fin Nat.zero)\nx : Fin Nat.zero → ℝ\nhxt : (Finset.sum n fun i => x i • t i) = 0\ni : ℕ\nhi : i < Nat.zero\nhin : { val := i, isLt := hi } ∈ n\n⊢ ¬False" :fullRange (:start (:line 86 :character 11) :end (:line 88 :character 48)))) :overlay-properties nil :overlay # :orig-beg 3588 :orig-end 3591) #s(flymake--diag :locus # :beg 4269 :end 4270 :type eglot-error :text "Lean 4: application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 103 :character 19) :end (:line 103 :character 20)) :message "application type mismatch\n ih s\nargument\n s\nhas type\n ↑(blades V (Nat.succ k)) : Type u_1\nbut is expected to have type\n Fin k → V : Type u_1" :fullRange (:start (:line 103 :character 19) :end (:line 103 :character 20)))) :overlay-properties nil :overlay # :orig-beg 4269 :orig-end 4270) #s(flymake--diag :locus # :beg 4376 :end 4379 :type eglot-error :text "Lean 4: function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 27) :end (:line 106 :character 30)) :message "function expected at\n v\nterm has type\n ExteriorAlgebra ℝ V" :fullRange (:start (:line 106 :character 27) :end (:line 106 :character 30)))) :overlay-properties nil :overlay # :orig-beg 4376 :orig-end 4379) #s(flymake--diag :locus # :beg 4439 :end 4440 :type eglot-error :text "Lean 4: application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 106 :character 90) :end (:line 106 :character 91)) :message "application type mismatch\n blade V v\nargument\n v\nhas type\n ExteriorAlgebra ℝ V : Type u_1\nbut is expected to have type\n Fin ?m.495318 → V : Type u_1" :fullRange (:start (:line 106 :character 90) :end (:line 106 :character 91)))) :overlay-properties nil :overlay # :orig-beg 4439 :orig-end 4440) #s(flymake--diag :locus # :beg 4462 :end 4466 :type eglot-error :text "Lean 4: unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :backend eglot-flymake-backend :data ((eglot-lsp-diag :source "Lean 4" :severity 1 :range (:start (:line 109 :character 4) :end (:line 109 :character 8)) :message "unsolved goals\ncase mpr\nV : Type u_1\ninst✝¹ : AddCommGroup V\ninst✝ : Module ℝ V\nk : ℕ\nt : Fin k → V\n⊢ (∀ (s : Finset (Fin k)) (g : Fin k → ℝ), (Finset.sum s fun i => g i • t i) = 0 → ∀ (i : Fin k), i ∈ s → g i = 0) →\n ↑(blade V t) ≠ 0" :fullRange (:start (:line 109 :character 4) :end (:line 109 :character 8)))) :overlay-properties nil :overlay # :orig-beg 4462 :orig-end 4466))) (cond (eglot--managed-mode (setq eglot--current-flymake-report-fn report-fn) (eglot--report-to-flymake eglot--diagnostics)) (t (funcall report-fn nil))) eglot-flymake-backend((closure ((buffer . #) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))))) :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043) apply(eglot-flymake-backend (closure ((buffer . #) (token . backend-token2723) (backend . eglot-flymake-backend)) (&rest args) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (apply #'flymake--handle-report backend token args))))) (:recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043)) (condition-case err (apply backend (flymake-make-report-fn backend run-token) args) ((debug error) (flymake--disable-backend backend err))) (let ((run-token (cl-gensym "backend-token"))) (let* ((b backend) (state (or (gethash b flymake--state) (puthash b (let (... ... ... ... ...) (progn ...)) flymake--state)))) (progn (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 1 run-token))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 3 nil))) (let* ((cl-x state)) (or (let* ((cl-x cl-x)) (progn (and ... t))) (signal 'wrong-type-argument (list 'flymake--state cl-x))) (let* ((v cl-x)) (aset v 2 nil))))) (condition-case err (apply backend (flymake-make-report-fn backend run-token) args) ((debug error) (flymake--disable-backend backend err)))) flymake--run-backend(eglot-flymake-backend (:recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043)) (cond ((and (not force) (let* ((b backend) (state (or (gethash b flymake--state) (puthash b ... flymake--state)))) (let* ((cl-x state)) (progn (or (let* ... ...) (signal ... ...)) (aref cl-x 3))))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) (closure ((backend-args :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043) (force)) (backend) (cond ((and (not force) (let* ((b backend) (state ...)) (let* (...) (progn ... ...)))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil)(eglot-flymake-backend) run-hook-wrapped((closure ((backend-args :recent-changes ((4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (4043 4043 "") (3966 3966 "") (3966 3966 "")) :changes-start 3966 :changes-end 4043) (force)) (backend) (cond ((and (not force) (let* ((b backend) (state ...)) (let* (...) (progn ... ...)))) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil) eglot-flymake-backend) (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start (cl-reduce #'min (mapcar #'car flymake--recent-changes)) :changes-end (cl-reduce #'max (mapcar #'cadr flymake--recent-changes)))))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* ((b backend) (state (or ... ...))) (let* ((cl-x state)) (or (let* ... ...) (signal ... ...)) (let* (...) (aset v 2 nil)))))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond ((and (not force) (let* ... ...)) (flymake--log-1 :debug 'flymake "Backend %s is disabled, not starting" backend)) (t (flymake--run-backend backend backend-args))) nil))) (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start (cl-reduce ... ...) :changes-end (cl-reduce ... ...))))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* (... ...) (let* ... ... ...)))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond (... ...) (t ...)) nil))))) (let (--cl-start-post-command-- --cl-start-on-display--) (setq --cl-start-post-command-- #'(lambda nil (progn (remove-hook 'post-command-hook --cl-start-post-command-- nil) (if (buffer-live-p buffer) (progn (save-current-buffer ... ...)))))) (setq --cl-start-on-display-- #'(lambda nil (progn (remove-hook 'window-configuration-change-hook --cl-start-on-display-- 'local) (flymake-start (remove 'on-display deferred) force)))) (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes (list :recent-changes flymake--recent-changes :changes-start ... :changes-end ...)))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (let* ... ...))) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda (backend) (cond ... ...) nil)))))) (let ((deferred (if (eq t deferred) '(post-command on-display) deferred)) (buffer (current-buffer))) (let (--cl-start-post-command-- --cl-start-on-display--) (setq --cl-start-post-command-- #'(lambda nil (progn (remove-hook 'post-command-hook --cl-start-post-command-- nil) (if (buffer-live-p buffer) (progn ...))))) (setq --cl-start-on-display-- #'(lambda nil (progn (remove-hook 'window-configuration-change-hook --cl-start-on-display-- 'local) (flymake-start (remove ... deferred) force)))) (cond ((and (memq 'post-command deferred) this-command) (add-hook 'post-command-hook --cl-start-post-command-- 'append nil)) ((and (memq 'on-display deferred) (not (get-buffer-window (current-buffer)))) (add-hook 'window-configuration-change-hook --cl-start-on-display-- 'append 'local)) (flymake-mode (setq flymake-check-start-time (float-time)) (let ((backend-args (and flymake--recent-changes ...))) (setq flymake--recent-changes nil) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda ... ...)) (run-hook-wrapped 'flymake-diagnostic-functions #'(lambda ... ... nil))))))) flymake-start(t) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t)) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil)) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil))) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug 'flymake "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil)))) (closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug ... "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil)))))(#) apply((closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn (flymake--log-1 :debug ... "starting syntax check after idle for %s seconds" flymake-no-changes-timeout) (flymake-start t))) (setq flymake-timer nil))))) #) timer-event-handler([t 0 0 500000 nil (closure (cl-struct-flymake--state-tags cl-struct-flymake--diag-tags t) (buffer) (if (buffer-live-p buffer) (progn (save-current-buffer (set-buffer buffer) (if (and flymake-mode flymake-no-changes-timeout) (progn ... ...)) (setq flymake-timer nil))))) (#) idle 0 nil])