Problem with emacs mode

[fblanqui]

The emacs-mode does not work anymore: File mode specification error: (error Quail key \varsubsetneqq is too long)

[gabrielhdt]

It must be because a prefix of \varsubsetneqq is already defined. I'll fix this (strange that I can't reproduce it).

[gabrielhdt]

Are you sure the error comes from the mode? Because \varsubsetneqq is not defined neither in https://github.com/vspinu/math-symbol-lists/blob/master/math-symbol-lists.el, nor in editors/emacs/lambdapi-input.el.

[fblanqui]

This is strange indeed because it was working well yesterday...

[gabrielhdt]

Perhaps restart your emacs and use M-x toggle-debug-on-error

[fblanqui]

I don't know why but the problem is related to 924b149b8bce1b3ff167b2d4d64e2e3f3c240ef4 because it works before but not after.

[fblanqui]

Note that, in this case, you can see that it would be useful to reintroduce a command make install_emacs so that make install do not replace a working emacs installation by a non-working one...

[gabrielhdt]

Note that, in this case, you can see that it would be useful to reintroduce a command make install_emacs so that make install do not replace a working emacs installation by a non-working one...

Perhaps I should have been more cautious when merging... Can you try to put (setq lambdapi-unicode-prefer-company 1) in your init.el?

[gabrielhdt]

And do you define any other quail rules, or abbrev?

[fblanqui]

No.

Le 19/04/2020 à 11:15, Gabriel Hondet a écrit :

And do you define any other quail rules, or abbrev?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/lambdapi/issues/362#issuecomment-616082966, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACSZRGPGDOC3KC6VPZ47ORLRNK6KHANCNFSM4MLJKVKA.

[fblanqui]

It indeed works if I do that and also add:

(add-hook 'lambdapi-mode-hook #'company-mode)

Le 19/04/2020 à 11:12, Gabriel Hondet a écrit :

Can you try to put |(setq lambdapi-unicode-prefer-company 1)| in your |init.el|?

[gabrielhdt]

It indeed works if I do that and also add: (add-hook 'lambdapi-mode-hook #'company-mode)

And can you complete (through quail) with \varsubsetneqq in this situation?

[fblanqui]

I get nothing but the message: Company: backend company-math-symbols-unicode error "Wrong type argument: char-or-string-p, nil" with args (post-completion varsubsetneqq).

[gabrielhdt]

I get nothing but the message: Company: backend company-math-symbols-unicode error "Wrong type argument: char-or-string-p, nil" with args (post-completion varsubsetneqq).

This is very strange because it looks like an error of company-math. Which version of company-math and company-math-symbols do you have?

[fblanqui]

More strangely in fact, nothing works if I do not use company at all!... Without company, I get the message File mode specification error: (error Quail key \varsubsetneqq is too long). So it rather looks like a bug in quail.

[fblanqui]

Btw do you know how to have completion in the minibuffer when we want to search/replace a string?

[gabrielhdt]

Btw do you know how to have completion in the minibuffer when we want to search/replace a string?

No, and I don't how emacs should know what you want to replace!

For your problem, I think you should post the debug report (obtained by calling M-x toggle-debug-on-error before the problem happens...).

[fblanqui]

Debugger entered--Lisp error: (error "Quail key \\varsubsetneqq is too long")
  signal(error ("Quail key \\varsubsetneqq is too long"))
  error("Quail key %s is too long" "\\varsubsetneqq")
  quail-defrule-internal("\\varsubsetneqq" nil (nil (96 nil (102 nil (90 ["ℨ"]) (122 ["𝔷"]) (89 ["𝔜"]) (121 ["𝔶"]) (88 ["𝔛"]) (120 ["𝔵"]) (87 ["𝔚"]) (119 ["𝔴"]) (86 ["𝔙"]) (118 ["𝔳"]) (85 ["𝔘"]) (117 ["𝔲"]) (84 ["𝔗"]) (116 ["𝔱"]) (83 ["𝔖"]) (115 ["𝔰"]) (82 ["ℜ"]) (114 ["𝔯"]) (81 ["𝔔"]) (113 ["𝔮"]) (80 ["𝔓"]) (112 ["𝔭"]) (79 ["𝔒"]) (111 ["𝔬"]) (78 ["𝔑"]) (110 ["𝔫"]) (77 ["𝔐"]) (109 ["𝔪"]) (76 ["𝔏"]) (108 ["𝔩"]) (75 ["𝔎"]) (107 ["𝔨"]) (74 ["𝔍"]) (106 ["𝔧"]) (73 ["ℑ"]) (105 ["𝔦"]) (72 ["ℌ"]) (104 ["𝔥"]) (71 ["𝔊"]) (103 ["𝔤"]) (70 ["𝔉"]) (102 ["𝔣"]) (69 ["𝔈"]) (101 ["𝔢"]) (68 ["𝔇"]) (100 ["𝔡"]) (67 ["ℭ"]) (99 ["𝔠"]) (66 ["𝔅"]) (98 ["𝔟"]) (65 ["𝔄"]) (97 ["𝔞"])) (73 nil (90 ["𝒁"]) (122 ["𝒛"]) (89 ["𝒀"]) (121 ["𝒚"]) (88 ["𝑿"]) (120 ["𝒙"]) (87 ["𝑾"]) (119 ["𝒘"]) (86 ["𝑽"]) (118 ["𝒗"]) (85 ["𝑼"]) (117 ["𝒖"]) (84 ["𝑻"]) (116 ["𝒕"]) (83 ["𝑺"]) (115 ["𝒔"]) (82 ["𝑹"]) (114 ["𝒓"]) (81 ["𝑸"]) (113 ["𝒒"]) (80 ["𝑷"]) (112 ["𝒑"]) (79 ["𝑶"]) (111 ["𝒐"]) (78 ["𝑵"]) (110 ["𝒏"]) (77 ["𝑴"]) (109 ["𝒎"]) (76 ["𝑳"]) (108 ["𝒍"]) (75 ["𝑲"]) (107 ["𝒌"]) (74 ["𝑱"]) (106 ["𝒋"]) (73 ["𝑰"]) (105 ["𝒊"]) (72 ["𝑯"]) (104 ["𝒉"]) (71 ["𝑮"]) (103 ["𝒈"]) (70 ["𝑭"]) (102 ["𝒇"]) (69 ["𝑬"]) (101 ["𝒆"]) (68 ["𝑫"]) (100 ["𝒅"]) (67 ["𝑪"]) (99 ["𝒄"]) (66 ["𝑩"]) (98 ["𝒃"]) (65 ["𝑨"]) (97 ["𝒂"])) (87 ["Ω"]) (119 ["ω"]) (120 ["χ"]) (85 ["ϒ"]) (117 ["υ"]) (116 ["τ"]) (83 ["Σ"] (90 ["𝓩"]) (122 ["𝔃"]) (89 ["𝓨"]) (121 ["𝔂"]) (88 ["𝓧"]) (120 ["𝔁"]) (87 ["𝓦"]) (119 ["𝔀"]) (86 ["𝓥"]) (118 ["𝓿"]) (85 ["𝓤"]) (117 ["𝓾"]) (84 ["𝓣"]) (116 ["𝓽"]) (83 ["𝓢"]) (115 ["𝓼"]) (82 ["𝓡"]) (114 ["𝓻"]) (81 ["𝓠"]) (113 ["𝓺"]) (80 ["𝓟"]) (112 ["𝓹"]) (79 ["𝓞"]) (111 ["𝓸"]) (78 ["𝓝"]) (110 ["𝓷"]) (77 ["𝓜"]) (109 ["𝓶"]) (76 ["𝓛"]) (108 ["𝓵"]) (75 ["𝓚"]) (107 ["𝓴"]) (74 ["𝓙"]) (106 ["𝓳"]) (73 ["𝓘"]) (105 ["𝓲"]) (72 ["𝓗"]) (104 ["𝓱"]) (71 ["𝓖"]) (103 ["𝓰"]) (70 ["𝓕"]) (102 ["𝓯"]) (69 ["𝓔"]) (101 ["𝓮"]) (68 ["𝓓"]) (100 ["𝓭"]) (67 ["𝓒"]) (99 ["𝓬"]) (66 ["𝓑"]) (98 ["𝓫"]) (65 ["𝓐"]) (97 ["𝓪"])) (115 ["σ"] (90 ["𝒵"]) (122 ["𝓏"]) (89 ["𝒴"]) (121 ["𝓎"]) (88 ["𝒳"]) (120 ["𝓍"]) (87 ["𝒲"]) (119 ["𝓌"]) (86 ["𝒱"]) (118 ["𝓋"]) (85 ["𝒰"]) (117 ["𝓊"]) (84 ["𝒯"]) (116 ["𝓉"]) (83 ["𝒮"]) (115 ["𝓈"]) (82 ["ℛ"]) (114 ["𝓇"]) (81 ["𝒬"]) (113 ["𝓆"]) (80 ["𝒫"]) (112 ["𝓅"]) (79 ["𝒪"]) (111 ["ℴ"]) (78 ["𝒩"]) (110 ["𝓃"]) (77 ["ℳ"]) (109 ["𝓂"]) (76 ["ℒ"]) (108 ["𝓁"]) (75 ["𝒦"]) (107 ["𝓀"]) (74 ["𝒥"]) (106 ["𝒿"]) (73 ["ℐ"]) (105 ["𝒾"]) (72 ["ℋ"]) (104 ["𝒽"]) (71 ["𝒢"]) (103 ["ℊ"]) (70 ["ℱ"]) (102 ["𝒻"]) (69 ["ℰ"]) (101 ["ℯ"]) (68 ["𝒟"]) (100 ["𝒹"]) (67 ["𝒞"]) (99 ["𝒸"]) (66 ["ℬ"]) (98 ["𝒷"]) (65 ["𝒜"]) (97 ["𝒶"])) (114 ["ρ"]) (80 ["Π"]) (112 ["π"]) (110 ["ν"]) (109 ["μ"]) (76 ["Λ"]) (108 ["λ"]) (107 ["κ"]) (105 ["ι"] (90 ["𝑍"]) (122 ["𝑧"]) (89 ["𝑌"]) (121 ["𝑦"]) (88 ["𝑋"]) (120 ["𝑥"]) (87 ["𝑊"]) (119 ["𝑤"]) (86 ["𝑉"]) (118 ["𝑣"]) (85 ["𝑈"]) (117 ["𝑢"]) (84 ["𝑇"]) (116 ["𝑡"]) (83 ["𝑆"]) (115 ["𝑠"]) (82 ["𝑅"]) (114 ["𝑟"]) (81 ["𝑄"]) (113 ["𝑞"]) (80 ["𝑃"]) (112 ["𝑝"]) (79 ["𝑂"]) (111 ["𝑜"]) (78 ["𝑁"]) (110 ["𝑛"]) (77 ["𝑀"]) (109 ["𝑚"]) (76 ["𝐿"]) (108 ["𝑙"]) (75 ["𝐾"]) (107 ["𝑘"]) (74 ["𝐽"]) (106 ["𝑗"]) (73 ["𝐼"]) (105 ["𝑖"]) (72 ["𝐻"]) (104 ["ℎ"]) (71 ["𝐺"]) (103 ["𝑔"]) (70 ["𝐹"]) (102 ["𝑓"]) (69 ["𝐸"]) (101 ["𝑒"]) (68 ["𝐷"]) (100 ["𝑑"]) (67 ["𝐶"]) (99 ["𝑐"]) (66 ["𝐵"]) (98 ["𝑏"]) (65 ["𝐴"]) (97 ["𝑎"])) (104 ["η"]) (122 ["ζ"]) (101 ["ε"]) (68 ["Δ"]) (100 ["δ"]) (67 ["Γ"]) (99 ["γ"]) (98 ["β"] (90 ["ℤ"]) (89 ["𝕐"]) (88 ["𝕏"]) (87 ["𝕎"]) (86 ["𝕍"]) (85 ["𝕌"]) (84 ["𝕋"]) (83 ["𝕊"]) (82 ["ℝ"]) (81 ["ℚ"]) (80 ["ℙ"]) (79 ["𝕆"]) (78 ["ℕ"]) (77 ["𝕄"]) (76 ["𝕃"]) (75 ["𝕂"]) (74 ["𝕁"]) (73 ["𝕀"]) (72 ["ℍ"]) (71 ["𝔾"]) (70 ["𝔽"]) (69 ["𝔼"]) (68 ["𝔻"]) (67 ["ℂ"]) (66 ["𝔹"]) (65 ["𝔸"])) (97 ["α"])) (94 nil (87 ["ᵂ"]) (86 ["ⱽ"]) (85 ["ᵁ"]) (84 ["ᵀ"]) (82 ["ᴿ"]) (80 ["ᴾ"]) (79 ["ᴼ"]) (78 ["ᴺ"]) (77 ["ᴹ"]) (76 ["ᴸ"]) (75 ["ᴷ"]) (74 ["ᴶ"]) (73 ["ᴵ"]) (72 ["ᴴ"]) (71 ["ᴳ"]) (69 ["ᴱ"]) (68 ["ᴰ"]) (66 ["ᴮ"]) (65 ["ᴬ"]) (122 ["ᶻ"]) (121 ["ʸ"]) (120 ["ˣ"]) (119 ["ʷ"]) (118 ["ᵛ"]) (117 ["ᵘ"]) (116 ["ᵗ"]) (115 ["ˢ"]) (114 ["ʳ"]) (112 ["ᵖ"]) (111 ["ᵒ"]) (110 ["ⁿ"]) (109 ["ᵐ"]) (108 ["ˡ"]) (107 ["ᵏ"]) (106 ["ʲ"]) (105 ["ⁱ"]) (104 ["ʰ"]) (103 ["ᵍ"]) (102 ["ᶠ"]) (101 ["ᵉ"]) (100 ["ᵈ"]) (99 ["ᶜ"]) (98 ["ᵇ"]) (97 ["ᵃ"]) (41 ["⁾"]) (40 ["⁽"]) (61 ["⁼"]) (45 ["⁻"]) (43 ["⁺"]) (57 ["⁹"]) (56 ["⁸"]) (55 ["⁷"]) (54 ["⁶"]) (53 ["⁵"]) (52 ["⁴"]) (51 ["³"]) (50 ["²"]) (49 ["¹"]) (48 ["⁰"])) (95 nil (120 ["ₓ"]) (118 ["ᵥ"]) (117 ["ᵤ"]) (116 ["ₜ"]) (115 ["ₛ"]) (114 ["ᵣ"]) (112 ["ₚ"]) (111 ["ₒ"]) (110 ["ₙ"]) (109 ["ₘ"]) (108 ["ₗ"]) (107 ["ₖ"]) (106 ["ⱼ"]) (105 ["ᵢ"]) (104 ["ₕ"]) (101 ["ₑ"]) (97 ["ₐ"]) (41 ["₎"]) (40 ["₍"]) (61 ["₌"]) (45 ["₋"]) (43 ["₊"]) (57 ["₉"]) (56 ["₈"]) (55 ["₇"]) (54 ["₆"]) (53 ["₅"]) (52 ["₄"]) (51 ["₃"]) (50 ["₂"]) (49 ["₁"]) (48 ["₀"])) (91 nil (93 ["□"])) (63 nil (63 ["∃"])) (126 nil (126 ["¬"])) (47 nil (92 ["∧"])) (38 nil (38 ["∧"])) (124 nil (124 ["∨"]) (45 ["⊢"])) (61 nil (41 ["⊃"]) (61 ["≡"])) (58 nil (58 ["⸬"]) (61 ["≔"])) (92 nil (86 nil (100 nil (97 nil (115 nil (104 8873)))) (118 nil (100 nil (97 nil (115 nil (104 8874)))))) (73 nil (109 8465)) (106 nil (109 nil (97 nil (116 nil (104 120485))))) (104 nil (101 nil (97 nil (114 nil (116 nil (115 nil (117 nil (105 nil (116 9825)))))))) (98 nil (97 nil (114 8463))) (111 nil (111 nil (107 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8618)))))))))) (108 nil (101 nil (102 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8617))))))))))))) (82 nil (115 nil (104 8625)) (101 8476) (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8658)))))))))) (102 nil (97 nil (108 nil (108 nil (105 nil (110 nil (103 nil (100 nil (111 nil (116 nil (115 nil (101 nil (113 8786)))))))))))) (108 nil (97 nil (116 9837))) (111 nil (114 nil (97 nil (108 nil (108 8704))))) (114 nil (111 nil (119 nil (110 8994))))) (74 nil (111 nil (105 nil (110 10781)))) (113 nil (101 nil (100 8718))) (119 nil (112 8472) (114 8768) (101 nil (100 nil (103 nil (101 8743))))) (79 nil (109 nil (101 nil (103 nil (97 937))))) (85 nil (112 nil (100 nil (111 nil (119 nil (110 nil (97 nil (114 nil (114 nil (111 nil (119 8661))))))))) (97 nil (114 nil (114 nil (111 nil (119 8657))))) (115 nil (105 nil (108 nil (111 nil (110 978))))))) (83 nil (117 nil (112 nil (115 nil (101 nil (116 8913)))) (98 nil (115 nil (101 nil (116 8912))))) (105 nil (103 nil (109 nil (97 931))))) (80 nil (115 nil (105 936)) (104 nil (105 934)) (105 928)) (88 nil (105 926)) (76 nil (115 nil (104 8624)) (108 nil (101 nil (102 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8666))))))))) (111 nil (110 nil (103 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 10233)))))))))) (108 nil (101 nil (102 nil (116 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 10234)))))))))) (97 nil (114 nil (114 nil (111 nil (119 10232)))))))))))) (101 nil (102 nil (116 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8660)))))))))) (97 nil (114 nil (114 nil (111 nil (119 8656)))))))) (97 nil (109 nil (98 nil (100 nil (97 923)))))) (84 nil (104 nil (101 nil (116 nil (97 920))))) (68 nil (105 nil (97 nil (109 nil (111 nil (110 nil (100)))))) (111 nil (119 nil (110 nil (97 nil (114 nil (114 nil (111 nil (119 8659)))))))) (101 nil (108 nil (116 nil (97 916))))) (71 nil (97 nil (109 nil (109 nil (97 915))))) (118 nil (68 nil (97 nil (115 nil (104 8872)))) (100 nil (97 nil (115 nil (104 8866)))) (101 nil (101 8744)) (97 nil (114 nil (79 nil (109 nil (101 nil (103 nil (97))))) (85 nil (112 nil (115 nil (105 nil (108 nil (111 nil (110))))))) (83 nil (105 nil (103 nil (109 nil (97))))) (80 nil (115 nil (105)) (104 nil (105)) (105)) (88 nil (105)) (76 nil (97 nil (109 nil (98 nil (100 nil (97)))))) (84 nil (104 nil (101 nil (116 nil (97))))) (68 nil (101 nil (108 nil (116 nil (97))))) (71 nil (97 nil (109 nil (109 nil (97))))) (115 nil (117 nil (98 nil (115 nil (101 nil (116 nil (110 nil (101 nil (113)))))))) (105 nil (103 nil (109 nil (97 962))))) (114 nil (104 nil (111 1009))) (112 nil (114 nil (111 nil (112 nil (116 nil (111 8733))))) (104 nil (105 966)) (105 982)) (116 nil (114 nil (105 nil (97 nil (110 nil (103 nil (108 nil (101 nil (114 nil (105 nil (103 nil (104 nil (116 8883))))) (108 nil (101 nil (102 nil (116 8882))))))))))) (104 nil (101 nil (116 nil (97 977))))) (101 nil (112 nil (115 nil (105 nil (108 nil (111 nil (110 949)))))))))) (99 nil (108 nil (117 nil (98 nil (115 nil (117 nil (105 nil (116 9827))))))) (111 nil (110 nil (103 8773))) (117 nil (114 nil (108 nil (121 nil (101 nil (113 nil (115 nil (117 nil (99 nil (99 8927)))) (112 nil (114 nil (101 nil (99 8926)))))))) (118 nil (101 nil (97 nil (114 nil (114 nil (111 nil (119 nil (114 nil (105 nil (103 nil (104 nil (116 8631))))) (108 nil (101 nil (102 nil (116 8630)))))))))))) (112 8746)) (97 nil (112 8745)) (100 nil (111 nil (116 8901))) (105 nil (114 nil (99 8728 (101 nil (113 8791)) (108 nil (101 nil (97 nil (114 nil (114 nil (111 nil (119 nil (114 nil (105 nil (103 nil (104 nil (116))))) (108 nil (101 nil (102 nil (116)))))))))))))) (104 nil (105 967))) (117 nil (110 nil (114 nil (104 nil (100))) (108 nil (104 nil (100)))) (112 nil (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (114 nil (105 nil (103 nil (104 nil (116 8638))))) (108 nil (101 nil (102 nil (116 8639))))))))))) (117 nil (112 nil (97 nil (114 nil (114 nil (111 nil (119 nil (115 8648)))))))) (100 nil (111 nil (119 nil (110 nil (97 nil (114 nil (114 nil (111 nil (119 8597))))))))) (97 nil (114 nil (114 nil (111 nil (119 8593))))) (108 nil (117 nil (115 8846))) (115 nil (105 nil (108 nil (111 nil (110 965))))))) (115 nil (112 nil (97 nil (100 nil (101 nil (115 nil (117 nil (105 nil (116 9824)))))))) (104 nil (111 nil (114 nil (116 nil (112 nil (97 nil (114 nil (97 nil (108 nil (108 nil (101 nil (108 8741)))))))) (109 nil (105 nil (100 8739)))))) (97 nil (114 nil (112 9839)))) (119 nil (97 nil (114 nil (114 nil (111 nil (119 8601)))))) (109 nil (97 nil (108 nil (108 nil (102 nil (114 nil (111 nil (119 nil (110 8994))))) (115 nil (109 nil (105 nil (108 nil (101 8995)))))))) (105 nil (108 nil (101 8995)))) (117 nil (114 nil (100 8730)) (112 nil (115 nil (101 nil (116 8835 (101 nil (113 8839 (113 10950))))))) (98 nil (115 nil (101 nil (116 8834 (110 nil (101 nil (113 8842 (113 10955)))) (101 nil (113 8838 (113 10949))))))) (99 nil (99 8827 (97 nil (112 nil (112 nil (114 nil (111 nil (120 10936)))))) (115 nil (105 nil (109 8831))) (99 nil (117 nil (114 nil (108 nil (121 nil (101 nil (113 8829))))))) (101 nil (113 10928))))) (101 nil (97 nil (114 nil (114 nil (111 nil (119 8600))))) (116 nil (109 nil (105 nil (110 nil (117 nil (115 8726))))))) (113 nil (115 nil (117 nil (112 nil (115 nil (101 nil (116 8848 (101 nil (113 8850)))))) (98 nil (115 nil (101 nil (116 8847 (101 nil (113 8849)))))))) (99 nil (97 nil (112 8851)))) (116 nil (97 nil (114 8902))) (105 nil (109 8764 (101 nil (113 8771))) (103 nil (109 nil (97 963))))) (114 nil (105 nil (115 nil (105 nil (110 nil (103 nil (100 nil (111 nil (116 nil (115 nil (101 nil (113 8787)))))))))) (103 nil (104 nil (116 nil (115 nil (113 nil (117 nil (105 nil (103 nil (97 nil (114 nil (114 nil (111 nil (119 8605)))))))))) (108 nil (101 nil (102 nil (116 nil (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (115 8652)))))))))))) (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (100 nil (111 nil (119 nil (110 8641)))) (117 nil (112 8640))))))))) (97 nil (114 nil (114 nil (111 nil (119 8594))))))))) (104 nil (100) (111 961))) (112 nil (97 nil (114 nil (116 nil (105 nil (97 nil (108 8706)))) (97 nil (108 nil (108 nil (101 nil (108 8741))))))) (101 nil (114 nil (112 10178))) (114 nil (105 nil (109 nil (101 8242))) (111 nil (112 nil (116 nil (111 8733)))) (101 nil (99 8826 (110 nil (97 nil (112 nil (112 nil (114 nil (111 nil (120 10937)))))) (115 nil (105 nil (109 8936)))) (97 nil (112 nil (112 nil (114 nil (111 nil (120 10935)))))) (115 nil (105 nil (109 8830))) (99 nil (117 nil (114 nil (108 nil (121 nil (101 nil (113 8828))))))) (101 nil (113 10927))))) (109 177) (115 nil (105 968)) (104 nil (105 981)) (105 960 (116 nil (99 nil (104 nil (102 nil (111 nil (114 nil (107 8916))))))))) (120 nil (105 958)) (110 nil (116 nil (114 nil (105 nil (97 nil (110 nil (103 nil (108 nil (101 nil (108 nil (101 nil (102 nil (116 8938 (101 nil (113 8940)))))))))))))) (118 nil (68 nil (97 nil (115 nil (104 8877)))) (100 nil (97 nil (115 nil (104 8876))))) (109 nil (105 nil (100 8740))) (115 nil (117 nil (98 nil (115 nil (101 nil (116 nil (101 nil (113 8840))))))) (104 nil (111 nil (114 nil (116 nil (109 nil (105 nil (100 8740))))))) (105 nil (109 8769))) (112 nil (114 nil (101 nil (99 8832 (101 nil (113)))))) (82 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8655)))))))))) (76 nil (101 nil (102 nil (116 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8654)))))))))) (97 nil (114 nil (114 nil (111 nil (119 8653))))))))) (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8603)))))))))) (108 nil (101 nil (113 8816 (113) (115 nil (108 nil (97 nil (110 nil (116)))))) (115 nil (115 8814)) (102 nil (116 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8622)))))))))) (97 nil (114 nil (114 nil (111 nil (119 8602))))))))) (111 nil (116 824)) (97 nil (116 nil (117 nil (114 nil (97 nil (108 9838))))) (98 nil (108 nil (97 8711)))) (119 nil (97 nil (114 nil (114 nil (111 nil (119 8598)))))) (105 8715) (101 nil (103 172) (97 nil (114 nil (114 nil (111 nil (119 8599))))) (113 8800)) (117 957)) (109 nil (104 nil (111 8487)) (97 nil (112 nil (115 nil (116 nil (111 8614))))) (105 nil (100 8739)) (111 nil (100 nil (101 nil (108 nil (115 8871))))) (112 8723) (117 956 (108 nil (116 nil (105 nil (109 nil (97 nil (112 8888)))))))) (108 nil (118 nil (101 nil (114 nil (116 nil (110 nil (101 nil (113 nil (113)))))))) (110 nil (97 nil (112 nil (112 nil (114 nil (111 nil (120 10889)))))) (115 nil (105 nil (109 8934))) (101 nil (113 10887 (113 8808)))) (111 nil (111 nil (112 nil (97 nil (114 nil (114 nil (111 nil (119 nil (114 nil (105 nil (103 nil (104 nil (116 8620))))) (108 nil (101 nil (102 nil (116 8619))))))))))) (110 nil (103 nil (109 nil (97 nil (112 nil (115 nil (116 nil (111 10236)))))) (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 10230)))))))))) (108 nil (101 nil (102 nil (116 nil (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 10231)))))))))) (97 nil (114 nil (114 nil (111 nil (119 10229)))))))))))) (108 8810 (108 8920)) (101 nil (115 nil (115 nil (101 nil (113 nil (113 nil (103 nil (116 nil (114 10891)))) (103 nil (116 nil (114 8922))))) (103 nil (116 nil (114 8822))) (100 nil (111 nil (116 8918))) (97 nil (112 nil (112 nil (114 nil (111 nil (120 10885)))))) (115 nil (105 nil (109 8818))))) (102 nil (116 nil (108 nil (101 nil (102 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 nil (115 8647)))))))))) (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (100 nil (111 nil (119 nil (110 8637)))) (117 nil (112 8636))))))))) (114 nil (105 nil (103 nil (104 nil (116 nil (115 nil (113 nil (117 nil (105 nil (103 nil (97 nil (114 nil (114 nil (111 nil (119 8621)))))))))) (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (115 8651)))))))) (97 nil (114 nil (114 nil (111 nil (119 8596 (115 8646))))))))))) (97 nil (114 nil (114 nil (111 nil (119 8592 (116 nil (97 nil (105 nil (108 8610))))))))))) (113 8804 (115 nil (108 nil (97 nil (110 nil (116 10877))))) (113 8806))) (104 nil (100)) (97 nil (109 nil (98 nil (100 nil (97 955)))))) (107 nil (97 nil (112 nil (112 nil (97 954))))) (105 nil (109 nil (97 nil (116 nil (104 305)))) (110 8712 (102 nil (116 nil (121 8734)))) (111 nil (116 nil (97 953)))) (116 nil (119 nil (111 nil (104 nil (101 nil (97 nil (100 nil (108 nil (101 nil (102 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119 8606))))))))))))))) (111 nil (112 8868)) (114 nil (105 nil (97 nil (110 nil (103 nil (108 nil (101 9651 (113 8796) (114 nil (105 nil (103 nil (104 nil (116 9655 (101 nil (113 8885))))))) (108 nil (101 nil (102 nil (116 9665 (101 nil (113 8884))))))))))))) (105 nil (109 nil (101 nil (115 215)))) (97 nil (117 964)) (104 nil (105 nil (99 nil (107 nil (97 nil (112 nil (112 nil (114 nil (111 nil (120 8776)))))) (115 nil (105 nil (109 8764)))))) (101 nil (114 nil (101 nil (102 nil (111 nil (114 nil (101 8756)))))) (116 nil (97 952))))) (122 nil (101 nil (116 nil (97 950)))) (101 nil (108 nil (108 8467)) (120 nil (105 nil (115 nil (116 nil (115 8707))))) (109 nil (112 nil (116 nil (121 nil (115 nil (101 nil (116 8709))))))) (113 nil (99 nil (105 nil (114 nil (99 8790)))) (115 nil (108 nil (97 nil (110 nil (116 nil (103 nil (116 nil (114 10902))) (108 nil (101 nil (115 nil (115 10901))))))))) (117 nil (105 nil (118 8801)))) (116 nil (97 951)) (112 nil (115 nil (105 nil (108 nil (111 nil (110 1013))))))) (103 nil (116 nil (114 nil (101 nil (113 nil (113 nil (108 nil (101 nil (115 nil (115 10892))))) (108 nil (101 nil (115 nil (115 8923)))))) (108 nil (101 nil (115 nil (115 8823)))) (100 nil (111 nil (116 8919))) (97 nil (112 nil (112 nil (114 nil (111 nil (120 10886)))))) (115 nil (105 nil (109 8819))))) (103 8811 (103 8921)) (101 nil (113 8805 (115 nil (108 nil (97 nil (110 nil (116 10878))))) (113 8807))) (97 nil (109 nil (109 nil (97 947))))) (98 nil (108 nil (97 nil (99 nil (107 nil (116 nil (114 nil (105 nil (97 nil (110 nil (103 nil (108 nil (101 nil (114 nil (105 nil (103 nil (104 nil (116 9654))))) (108 nil (101 nil (102 nil (116 9664)))))))))))))))) (97 nil (99 nil (107 nil (101 nil (112 nil (115 nil (105 nil (108 nil (111 nil (110 1014))))))) (115 nil (105 nil (109 8765 (101 nil (113 8909)))))))) (111 nil (116 8869) (119 nil (116 nil (105 nil (101 8904))))) (105 nil (103 nil (99 nil (105 nil (114 nil (99 9675)))) (116 nil (114 nil (105 nil (97 nil (110 nil (103 nil (108 nil (101 nil (100 nil (111 nil (119 nil (110 9661)))) (117 nil (112 9651)))))))))))) (117 nil (109 nil (112 nil (101 nil (113 8783)))) (108 nil (108 nil (101 nil (116 8729))))) (101 nil (99 nil (97 nil (117 nil (115 nil (101 8757))))) (116 nil (119 nil (101 nil (101 nil (110 8812)))) (97 946)))) (66 nil (117 nil (109 nil (112 nil (101 nil (113 8782))))) (111 nil (120))) (47 ["∨"]) (111 nil (100 nil (111 nil (116 8857))) (115 nil (108 nil (97 nil (115 nil (104 8709))))) (116 nil (105 nil (109 nil (101 nil (115 8855))))) (112 nil (108 nil (117 nil (115 8853)))) (109 nil (105 nil (110 nil (117 nil (115 8854)))) (101 nil (103 nil (97 969)))) (114 ["∨"])) (97 nil (112 nil (112 nil (114 nil (111 nil (120 8776 (101 nil (113 8778))))))) (109 nil (97 nil (108 nil (103 10815)))) (115 nil (121 nil (109 nil (112 8781))) (116 8727)) (108 nil (101 nil (112 nil (104 8501))) (112 nil (104 nil (97 945)))) (110 nil (103 nil (108 nil (101 8736))) (100 ["∧"]))) (100 nil (111 nil (119 nil (110 nil (100 nil (111 nil (119 nil (110 nil (97 nil (114 nil (114 nil (111 nil (119 nil (115 8650)))))))))) (104 nil (97 nil (114 nil (112 nil (111 nil (111 nil (110 nil (114 nil (105 nil (103 nil (104 nil (116 8642))))) (108 nil (101 nil (102 nil (116 8643))))))))))) (97 nil (114 nil (114 nil (111 nil (119 8595))))))) (116 nil (101 nil (113 8784 (100 nil (111 nil (116))))))) (100 nil (97 nil (103 nil (103 nil (101 nil (114 8225)))))) (97 nil (115 nil (104 nil (108 nil (101 nil (102 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119))))))))) (114 nil (105 nil (103 nil (104 nil (116 nil (97 nil (114 nil (114 nil (111 nil (119)))))))))) (118 8867))) (103 nil (103 nil (101 nil (114 8224))))) (105 nil (97 nil (109 nil (111 nil (110 nil (100 8900 (115 nil (117 nil (105 nil (116 9826))))))))) (118 247)) (101 nil (108 nil (116 nil (97 948))) (102 nil (101 nil (113 ((0 0 0 0 nil) . [8788 "≔"])))))) (92 ["λ"])) (33 nil (33 ["Π"])) (45 nil (45 nil (62 ["↪"])) (62 ["→"]))) nil)
  quail-defrule("\\varsubsetneqq" nil)
  (closure (t) (com-ltx) (quail-defrule (car com-ltx) (cdr com-ltx)))(("\\varsubsetneqq"))
  mapc((closure (t) (com-ltx) (quail-defrule (car com-ltx) (cdr com-ltx))) (("\\alpha" 945) ("\\beta" 946) ("\\gamma" 947) ("\\delta" 948) ("\\epsilon" 1013) ("\\zeta" 950) ("\\eta" 951) ("\\theta" 952) ("\\iota" 953) ("\\kappa" 954) ("\\lambda" 955) ("\\mu" 956) ("\\nu" 957) ("\\xi" 958) ("\\pi" 960) ("\\rho" 961) ("\\sigma" 963) ("\\tau" 964) ("\\upsilon" 965) ("\\phi" 981) ("\\chi" 967) ("\\psi" 968) ("\\omega" 969) ("\\varepsilon" 949) ("\\vartheta" 977) ("\\varpi" 982) ("\\varrho" 1009) ("\\varsigma" 962) ("\\varphi" 966) ("\\Gamma" 915) ("\\Delta" 916) ("\\Theta" 920) ("\\Lambda" 923) ("\\Xi" 926) ("\\Pi" 928) ("\\Sigma" 931) ("\\Upsilon" 978) ("\\Phi" 934) ("\\Psi" 936) ("\\Omega" 937) ("\\pm" 177) ("\\mp" 8723) ("\\times" 215) ("\\div" 247) ("\\ast" 8727) ("\\star" 8902) ("\\circ" 8728) ("\\bullet" 8729) ("\\cdot" 8901) ("\\cap" 8745) ("\\cup" 8746) ("\\uplus" 8846) ("\\sqcap" 8851) ("\\vee" 8744) ("\\wedge" 8743) ("\\setminus" 8726) ("\\wr" 8768) ("\\diamond" 8900) ("\\bigtriangleup" 9651) ("\\bigtriangledown" 9661) ("\\triangleleft" 9665) ("\\triangleright" 9655) ("\\lhd") ("\\rhd") ("\\unlhd") ("\\unrhd") ("\\oplus" 8853) ("\\ominus" 8854) ("\\otimes" 8855) ("\\oslash" 8709) ("\\odot" 8857) ("\\bigcirc" 9675) ("\\dagger" 8224) ("\\ddagger" 8225) ("\\amalg" 10815) ("\\leq" 8804) ("\\geq" 8805) ("\\qed" 8718) ("\\equiv" 8801) ("\\models" 8871) ("\\prec" 8826) ("\\succ" 8827) ("\\sim" 8764) ("\\perp" 10178) ("\\preceq" 10927) ("\\succeq" 10928) ("\\simeq" 8771) ("\\mid" 8739) ("\\ll" 8810) ("\\gg" 8811) ("\\asymp" 8781) ("\\parallel" 8741) ("\\subset" 8834) ("\\supset" 8835) ("\\approx" 8776) ("\\bowtie" 8904) ("\\subseteq" 8838) ("\\supseteq" 8839) ("\\cong" 8773) ("\\Join" 10781) ("\\sqsubset" 8847) ("\\sqsupset" 8848) ("\\neq" 8800) ("\\smile" 8995) ("\\sqsubseteq" 8849) ("\\sqsupseteq" 8850) ("\\doteq" 8784) ("\\frown" 8994) ("\\in" 8712) ("\\ni" 8715) ("\\propto" 8733) ("\\vdash" 8866) ("\\dashv" 8867) ("\\leftarrow" 8592) ("\\Leftarrow" 8656) ("\\rightarrow" 8594) ("\\Rightarrow" 8658) ("\\leftrightarrow" 8596) ("\\Leftrightarrow" 8660) ("\\mapsto" 8614) ("\\hookleftarrow" 8617) ("\\leftharpoonup" 8636) ("\\leftharpoondown" 8637) ("\\longleftarrow" 10229) ("\\Longleftarrow" 10232) ("\\longrightarrow" 10230) ("\\Longrightarrow" 10233) ("\\longleftrightarrow" 10231) ("\\Longleftrightarrow" 10234) ("\\longmapsto" 10236) ("\\hookrightarrow" 8618) ("\\rightharpoonup" 8640) ("\\rightharpoondown" 8641) ("\\uparrow" 8593) ("\\Uparrow" 8657) ("\\downarrow" 8595) ("\\Downarrow" 8659) ("\\updownarrow" 8597) ("\\Updownarrow" 8661) ("\\nearrow" 8599) ("\\searrow" 8600) ("\\swarrow" 8601) ("\\nwarrow" 8598) ("\\nabla" 8711) ("\\aleph" 8501) ("\\prime" 8242) ("\\forall" 8704) ("\\infty" 8734) ("\\hbar" 8463) ("\\emptyset" 8709) ("\\exists" 8707) ("\\surd" 8730) ("\\Box") ("\\triangle" 9651) ("\\Diamond") ("\\imath" 305) ("\\jmath" 120485) ("\\ell" 8467) ("\\neg" 172) ("\\not" 824) ("\\top" 8868) ("\\flat" 9837) ("\\natural" 9838) ("\\sharp" 9839) ("\\wp" 8472) ("\\bot" 8869) ("\\clubsuit" 9827) ("\\diamondsuit" 9826) ("\\heartsuit" 9825) ("\\spadesuit" 9824) ("\\mho" 8487) ("\\Re" 8476) ("\\Im" 8465) ("\\angle" 8736) ("\\partial" 8706) ("\\varGamma") ("\\varDelta") ("\\varTheta") ("\\varLambda") ("\\varXi") ("\\varPi") ("\\varSigma") ("\\varUpsilon") ("\\varPhi") ("\\varPsi") ("\\varOmega") ("\\dashrightarrow") ("\\dashleftarrow") ("\\leftleftarrows" 8647) ("\\leftrightarrows" 8646) ("\\Lleftarrow" 8666) ("\\twoheadleftarrow" 8606) ("\\leftarrowtail" 8610) ("\\looparrowleft" 8619) ("\\leftrightharpoons" 8651) ("\\curvearrowleft" 8630) ("\\circlearrowleft") ("\\Lsh" 8624) ("\\upuparrows" 8648) ("\\upharpoonleft" 8639) ("\\downharpoonleft" 8643) ("\\multimap" 8888) ("\\leftrightsquigarrow" 8621) ("\\looparrowright" 8620) ("\\rightleftharpoons" 8652) ("\\curvearrowright" 8631) ("\\circlearrowright") ("\\Rsh" 8625) ("\\downdownarrows" 8650) ("\\upharpoonright" 8638) ("\\downharpoonright" 8642) ("\\rightsquigarrow" 8605) ("\\nleftarrow" 8602) ("\\nrightarrow" 8603) ("\\nLeftarrow" 8653) ("\\nRightarrow" 8655) ("\\nleftrightarrow" 8622) ("\\nLeftrightarrow" 8654) ("\\leqq" 8806) ("\\leqslant" 10877) ("\\eqslantless" 10901) ("\\lesssim" 8818) ("\\lessapprox" 10885) ("\\approxeq" 8778) ("\\lessdot" 8918) ("\\lll" 8920) ("\\lessgtr" 8822) ("\\lesseqgtr" 8922) ("\\lesseqqgtr" 10891) ("\\doteqdot") ("\\risingdotseq" 8787) ("\\fallingdotseq" 8786) ("\\backsim" 8765) ("\\backsimeq" 8909) ("\\subseteqq" 10949) ("\\Subset" 8912) ("\\sqsubset" 8847) ("\\preccurlyeq" 8828) ("\\curlyeqprec" 8926) ("\\precsim" 8830) ("\\precapprox" 10935) ("\\vartriangleleft" 8882) ("\\trianglelefteq" 8884) ("\\vDash" 8872) ("\\Vvdash" 8874) ("\\smallsmile" 8995) ("\\smallfrown" 8994) ("\\bumpeq" 8783) ("\\Bumpeq" 8782) ("\\geqq" 8807) ("\\geqslant" 10878) ("\\eqslantgtr" 10902) ("\\gtrsim" 8819) ("\\gtrapprox" 10886) ("\\gtrdot" 8919) ("\\ggg" 8921) ("\\gtrless" 8823) ("\\gtreqless" 8923) ("\\gtreqqless" 10892) ("\\eqcirc" 8790) ("\\circeq" 8791) ("\\triangleq" 8796) ("\\thicksim" 8764) ("\\thickapprox" 8776) ("\\supseteqq" 10950) ("\\Supset" 8913) ("\\sqsupset" 8848) ("\\succcurlyeq" 8829) ("\\curlyeqsucc" 8927) ("\\succsim" 8831) ("\\succapprox" 10936) ("\\vartriangleright" 8883) ("\\trianglerighteq" 8885) ("\\Vdash" 8873) ("\\shortmid" 8739) ("\\shortparallel" 8741) ("\\between" 8812) ("\\pitchfork" 8916) ("\\varpropto" 8733) ("\\blacktriangleleft" 9664) ("\\therefore" 8756) ("\\backepsilon" 1014) ("\\blacktriangleright" 9654) ("\\because" 8757) ("\\nless" 8814) ("\\nleq" 8816) ("\\nleqslant") ("\\nleqq") ("\\lneq" 10887) ("\\lneqq" 8808) ("\\lvertneqq") ("\\lnsim" 8934) ("\\lnapprox" 10889) ("\\nprec" 8832) ("\\npreceq") ("\\precnsim" 8936) ("\\precnapprox" 10937) ("\\nsim" 8769) ("\\nshortmid" 8740) ("\\nmid" 8740) ("\\nvdash" 8876) ("\\nvDash" 8877) ("\\ntriangleleft" 8938) ("\\ntrianglelefteq" 8940) ("\\nsubseteq" 8840) ("\\subsetneq" 8842) ("\\varsubsetneq") ("\\subsetneqq" 10955) ("\\varsubsetneqq") ("\\ngtr" 8815) ("\\ngeq" 8817) ("\\ngeqslant") ("\\ngeqq") ("\\gneq" 10888) ("\\gneqq" 8809) ("\\gvertneqq") ("\\gnsim" 8935) ("\\gnapprox" 10890) ("\\nsucc" 8833) ("\\nsucceq") ("\\succnsim" 8937) ("\\succnapprox" 10938) ("\\ncong" 8775) ("\\nshortparallel" 8742) ("\\nparallel" 8742) ("\\nvDash" 8877) ("\\nVDash" 8879) ("\\ntriangleright" 8939) ("\\ntrianglerighteq" 8941) ("\\nsupseteq" 8841) ("\\nsupseteqq") ("\\supsetneq" 8843) ("\\varsupsetneq") ("\\supsetneqq" 10956) ("\\varsupsetneqq") ("\\dotplus" 8724) ("\\smallsetminus" 8726) ("\\Cap" 8914) ("\\Cup" 8915) ("\\barwedge" 8892) ("\\veebar" 8891) ("\\doublebarwedge" 8966) ("\\boxminus" 8863) ("\\boxtimes" 8864) ("\\boxdot" 8865) ("\\boxplus" 8862) ("\\divideontimes" 8903) ("\\ltimes" 8905) ("\\rtimes" 8906) ("\\leftthreetimes" 8907) ("\\rightthreetimes" 8908) ("\\curlywedge" 8911) ("\\curlyvee" 8910) ("\\circleddash" 8861) ("\\circledast" 8859) ("\\circledcirc" 8858) ("\\centerdot") ("\\intercal" 8890) ("\\hbar" 8463) ("\\hslash" 8463) ("\\vartriangle" 9653) ("\\triangledown" 9663) ("\\square" 9633) ("\\lozenge" 9674) ("\\circledS" 9416) ("\\angle" 8736) ("\\measuredangle" 8737) ("\\nexists" 8708) ("\\mho" 8487) ("\\Finv" 8498) ("\\Game" 8513) ("\\Bbbk" 120156) ("\\backprime" 8245) ("\\varnothing" 8709) ("\\blacktriangle" 9652) ("\\blacktriangledown" 9662) ("\\blacksquare" 9632) ("\\blacklozenge" 10731) ("\\bigstar" 9733) ("\\sphericalangle" 8738) ("\\complement" 8705) ("\\eth" 240) ("\\diagup" 9585) ("\\diagdown" 9586) ("\\BbbC") ("\\BbbH") ("\\BbbN") ("\\BbbP") ("\\BbbQ") ("\\BbbR") ("\\BbbZ") ("\\Bbbpi") ("\\Bbbgamma") ("\\BbbGamma") ("\\BbbPi") ("\\Bbbsum") ("\\mitBbbD") ("\\mitBbbd") ("\\mitBbbe") ("\\mitBbbi") ("\\mitBbbj") ("\\BbbA") ("\\BbbB") ("\\BbbD") ("\\BbbE") ("\\BbbF") ("\\BbbG") ("\\BbbI") ("\\BbbJ") ("\\BbbK") ("\\BbbL") ("\\BbbM") ("\\BbbO") ("\\BbbS") ("\\BbbT") ("\\BbbU") ("\\BbbV") ("\\BbbW") ("\\BbbX") ("\\BbbY") ("\\Bbba") ("\\Bbbb") ("\\Bbbc") ("\\Bbbd") ("\\Bbbe") ("\\Bbbf") ("\\Bbbg") ("\\Bbbh") ("\\Bbbi") ("\\Bbbj") ("\\Bbbk") ("\\Bbbl") ("\\Bbbm") ("\\Bbbn") ("\\Bbbo") ("\\Bbbp") ("\\Bbbq") ("\\Bbbr") ("\\Bbbs") ("\\Bbbt") ("\\Bbbu") ("\\Bbbv") ("\\Bbbw") ("\\Bbbx") ("\\Bbby") ("\\Bbbz") ("\\Bbbzero") ("\\Bbbone") ("\\Bbbtwo") ("\\Bbbthree") ("\\Bbbfour") ("\\Bbbfive") ("\\Bbbsix") ("\\Bbbseven") ("\\Bbbeight") ("\\Bbbnine")))
  seq-do((closure (t) (com-ltx) (quail-defrule (car com-ltx) (cdr com-ltx))) (("\\alpha" 945) ("\\beta" 946) ("\\gamma" 947) ("\\delta" 948) ("\\epsilon" 1013) ("\\zeta" 950) ("\\eta" 951) ("\\theta" 952) ("\\iota" 953) ("\\kappa" 954) ("\\lambda" 955) ("\\mu" 956) ("\\nu" 957) ("\\xi" 958) ("\\pi" 960) ("\\rho" 961) ("\\sigma" 963) ("\\tau" 964) ("\\upsilon" 965) ("\\phi" 981) ("\\chi" 967) ("\\psi" 968) ("\\omega" 969) ("\\varepsilon" 949) ("\\vartheta" 977) ("\\varpi" 982) ("\\varrho" 1009) ("\\varsigma" 962) ("\\varphi" 966) ("\\Gamma" 915) ("\\Delta" 916) ("\\Theta" 920) ("\\Lambda" 923) ("\\Xi" 926) ("\\Pi" 928) ("\\Sigma" 931) ("\\Upsilon" 978) ("\\Phi" 934) ("\\Psi" 936) ("\\Omega" 937) ("\\pm" 177) ("\\mp" 8723) ("\\times" 215) ("\\div" 247) ("\\ast" 8727) ("\\star" 8902) ("\\circ" 8728) ("\\bullet" 8729) ("\\cdot" 8901) ("\\cap" 8745) ("\\cup" 8746) ("\\uplus" 8846) ("\\sqcap" 8851) ("\\vee" 8744) ("\\wedge" 8743) ("\\setminus" 8726) ("\\wr" 8768) ("\\diamond" 8900) ("\\bigtriangleup" 9651) ("\\bigtriangledown" 9661) ("\\triangleleft" 9665) ("\\triangleright" 9655) ("\\lhd") ("\\rhd") ("\\unlhd") ("\\unrhd") ("\\oplus" 8853) ("\\ominus" 8854) ("\\otimes" 8855) ("\\oslash" 8709) ("\\odot" 8857) ("\\bigcirc" 9675) ("\\dagger" 8224) ("\\ddagger" 8225) ("\\amalg" 10815) ("\\leq" 8804) ("\\geq" 8805) ("\\qed" 8718) ("\\equiv" 8801) ("\\models" 8871) ("\\prec" 8826) ("\\succ" 8827) ("\\sim" 8764) ("\\perp" 10178) ("\\preceq" 10927) ("\\succeq" 10928) ("\\simeq" 8771) ("\\mid" 8739) ("\\ll" 8810) ("\\gg" 8811) ("\\asymp" 8781) ("\\parallel" 8741) ("\\subset" 8834) ("\\supset" 8835) ("\\approx" 8776) ("\\bowtie" 8904) ("\\subseteq" 8838) ("\\supseteq" 8839) ("\\cong" 8773) ("\\Join" 10781) ("\\sqsubset" 8847) ("\\sqsupset" 8848) ("\\neq" 8800) ("\\smile" 8995) ("\\sqsubseteq" 8849) ("\\sqsupseteq" 8850) ("\\doteq" 8784) ("\\frown" 8994) ("\\in" 8712) ("\\ni" 8715) ("\\propto" 8733) ("\\vdash" 8866) ("\\dashv" 8867) ("\\leftarrow" 8592) ("\\Leftarrow" 8656) ("\\rightarrow" 8594) ("\\Rightarrow" 8658) ("\\leftrightarrow" 8596) ("\\Leftrightarrow" 8660) ("\\mapsto" 8614) ("\\hookleftarrow" 8617) ("\\leftharpoonup" 8636) ("\\leftharpoondown" 8637) ("\\longleftarrow" 10229) ("\\Longleftarrow" 10232) ("\\longrightarrow" 10230) ("\\Longrightarrow" 10233) ("\\longleftrightarrow" 10231) ("\\Longleftrightarrow" 10234) ("\\longmapsto" 10236) ("\\hookrightarrow" 8618) ("\\rightharpoonup" 8640) ("\\rightharpoondown" 8641) ("\\uparrow" 8593) ("\\Uparrow" 8657) ("\\downarrow" 8595) ("\\Downarrow" 8659) ("\\updownarrow" 8597) ("\\Updownarrow" 8661) ("\\nearrow" 8599) ("\\searrow" 8600) ("\\swarrow" 8601) ("\\nwarrow" 8598) ("\\nabla" 8711) ("\\aleph" 8501) ("\\prime" 8242) ("\\forall" 8704) ("\\infty" 8734) ("\\hbar" 8463) ("\\emptyset" 8709) ("\\exists" 8707) ("\\surd" 8730) ("\\Box") ("\\triangle" 9651) ("\\Diamond") ("\\imath" 305) ("\\jmath" 120485) ("\\ell" 8467) ("\\neg" 172) ("\\not" 824) ("\\top" 8868) ("\\flat" 9837) ("\\natural" 9838) ("\\sharp" 9839) ("\\wp" 8472) ("\\bot" 8869) ("\\clubsuit" 9827) ("\\diamondsuit" 9826) ("\\heartsuit" 9825) ("\\spadesuit" 9824) ("\\mho" 8487) ("\\Re" 8476) ("\\Im" 8465) ("\\angle" 8736) ("\\partial" 8706) ("\\varGamma") ("\\varDelta") ("\\varTheta") ("\\varLambda") ("\\varXi") ("\\varPi") ("\\varSigma") ("\\varUpsilon") ("\\varPhi") ("\\varPsi") ("\\varOmega") ("\\dashrightarrow") ("\\dashleftarrow") ("\\leftleftarrows" 8647) ("\\leftrightarrows" 8646) ("\\Lleftarrow" 8666) ("\\twoheadleftarrow" 8606) ("\\leftarrowtail" 8610) ("\\looparrowleft" 8619) ("\\leftrightharpoons" 8651) ("\\curvearrowleft" 8630) ("\\circlearrowleft") ("\\Lsh" 8624) ("\\upuparrows" 8648) ("\\upharpoonleft" 8639) ("\\downharpoonleft" 8643) ("\\multimap" 8888) ("\\leftrightsquigarrow" 8621) ("\\looparrowright" 8620) ("\\rightleftharpoons" 8652) ("\\curvearrowright" 8631) ("\\circlearrowright") ("\\Rsh" 8625) ("\\downdownarrows" 8650) ("\\upharpoonright" 8638) ("\\downharpoonright" 8642) ("\\rightsquigarrow" 8605) ("\\nleftarrow" 8602) ("\\nrightarrow" 8603) ("\\nLeftarrow" 8653) ("\\nRightarrow" 8655) ("\\nleftrightarrow" 8622) ("\\nLeftrightarrow" 8654) ("\\leqq" 8806) ("\\leqslant" 10877) ("\\eqslantless" 10901) ("\\lesssim" 8818) ("\\lessapprox" 10885) ("\\approxeq" 8778) ("\\lessdot" 8918) ("\\lll" 8920) ("\\lessgtr" 8822) ("\\lesseqgtr" 8922) ("\\lesseqqgtr" 10891) ("\\doteqdot") ("\\risingdotseq" 8787) ("\\fallingdotseq" 8786) ("\\backsim" 8765) ("\\backsimeq" 8909) ("\\subseteqq" 10949) ("\\Subset" 8912) ("\\sqsubset" 8847) ("\\preccurlyeq" 8828) ("\\curlyeqprec" 8926) ("\\precsim" 8830) ("\\precapprox" 10935) ("\\vartriangleleft" 8882) ("\\trianglelefteq" 8884) ("\\vDash" 8872) ("\\Vvdash" 8874) ("\\smallsmile" 8995) ("\\smallfrown" 8994) ("\\bumpeq" 8783) ("\\Bumpeq" 8782) ("\\geqq" 8807) ("\\geqslant" 10878) ("\\eqslantgtr" 10902) ("\\gtrsim" 8819) ("\\gtrapprox" 10886) ("\\gtrdot" 8919) ("\\ggg" 8921) ("\\gtrless" 8823) ("\\gtreqless" 8923) ("\\gtreqqless" 10892) ("\\eqcirc" 8790) ("\\circeq" 8791) ("\\triangleq" 8796) ("\\thicksim" 8764) ("\\thickapprox" 8776) ("\\supseteqq" 10950) ("\\Supset" 8913) ("\\sqsupset" 8848) ("\\succcurlyeq" 8829) ("\\curlyeqsucc" 8927) ("\\succsim" 8831) ("\\succapprox" 10936) ("\\vartriangleright" 8883) ("\\trianglerighteq" 8885) ("\\Vdash" 8873) ("\\shortmid" 8739) ("\\shortparallel" 8741) ("\\between" 8812) ("\\pitchfork" 8916) ("\\varpropto" 8733) ("\\blacktriangleleft" 9664) ("\\therefore" 8756) ("\\backepsilon" 1014) ("\\blacktriangleright" 9654) ("\\because" 8757) ("\\nless" 8814) ("\\nleq" 8816) ("\\nleqslant") ("\\nleqq") ("\\lneq" 10887) ("\\lneqq" 8808) ("\\lvertneqq") ("\\lnsim" 8934) ("\\lnapprox" 10889) ("\\nprec" 8832) ("\\npreceq") ("\\precnsim" 8936) ("\\precnapprox" 10937) ("\\nsim" 8769) ("\\nshortmid" 8740) ("\\nmid" 8740) ("\\nvdash" 8876) ("\\nvDash" 8877) ("\\ntriangleleft" 8938) ("\\ntrianglelefteq" 8940) ("\\nsubseteq" 8840) ("\\subsetneq" 8842) ("\\varsubsetneq") ("\\subsetneqq" 10955) ("\\varsubsetneqq") ("\\ngtr" 8815) ("\\ngeq" 8817) ("\\ngeqslant") ("\\ngeqq") ("\\gneq" 10888) ("\\gneqq" 8809) ("\\gvertneqq") ("\\gnsim" 8935) ("\\gnapprox" 10890) ("\\nsucc" 8833) ("\\nsucceq") ("\\succnsim" 8937) ("\\succnapprox" 10938) ("\\ncong" 8775) ("\\nshortparallel" 8742) ("\\nparallel" 8742) ("\\nvDash" 8877) ("\\nVDash" 8879) ("\\ntriangleright" 8939) ("\\ntrianglerighteq" 8941) ("\\nsupseteq" 8841) ("\\nsupseteqq") ("\\supsetneq" 8843) ("\\varsupsetneq") ("\\supsetneqq" 10956) ("\\varsupsetneqq") ("\\dotplus" 8724) ("\\smallsetminus" 8726) ("\\Cap" 8914) ("\\Cup" 8915) ("\\barwedge" 8892) ("\\veebar" 8891) ("\\doublebarwedge" 8966) ("\\boxminus" 8863) ("\\boxtimes" 8864) ("\\boxdot" 8865) ("\\boxplus" 8862) ("\\divideontimes" 8903) ("\\ltimes" 8905) ("\\rtimes" 8906) ("\\leftthreetimes" 8907) ("\\rightthreetimes" 8908) ("\\curlywedge" 8911) ("\\curlyvee" 8910) ("\\circleddash" 8861) ("\\circledast" 8859) ("\\circledcirc" 8858) ("\\centerdot") ("\\intercal" 8890) ("\\hbar" 8463) ("\\hslash" 8463) ("\\vartriangle" 9653) ("\\triangledown" 9663) ("\\square" 9633) ("\\lozenge" 9674) ("\\circledS" 9416) ("\\angle" 8736) ("\\measuredangle" 8737) ("\\nexists" 8708) ("\\mho" 8487) ("\\Finv" 8498) ("\\Game" 8513) ("\\Bbbk" 120156) ("\\backprime" 8245) ("\\varnothing" 8709) ("\\blacktriangle" 9652) ("\\blacktriangledown" 9662) ("\\blacksquare" 9632) ("\\blacklozenge" 10731) ("\\bigstar" 9733) ("\\sphericalangle" 8738) ("\\complement" 8705) ("\\eth" 240) ("\\diagup" 9585) ("\\diagdown" 9586) ("\\BbbC") ("\\BbbH") ("\\BbbN") ("\\BbbP") ("\\BbbQ") ("\\BbbR") ("\\BbbZ") ("\\Bbbpi") ("\\Bbbgamma") ("\\BbbGamma") ("\\BbbPi") ("\\Bbbsum") ("\\mitBbbD") ("\\mitBbbd") ("\\mitBbbe") ("\\mitBbbi") ("\\mitBbbj") ("\\BbbA") ("\\BbbB") ("\\BbbD") ("\\BbbE") ("\\BbbF") ("\\BbbG") ("\\BbbI") ("\\BbbJ") ("\\BbbK") ("\\BbbL") ("\\BbbM") ("\\BbbO") ("\\BbbS") ("\\BbbT") ("\\BbbU") ("\\BbbV") ("\\BbbW") ("\\BbbX") ("\\BbbY") ("\\Bbba") ("\\Bbbb") ("\\Bbbc") ("\\Bbbd") ("\\Bbbe") ("\\Bbbf") ("\\Bbbg") ("\\Bbbh") ("\\Bbbi") ("\\Bbbj") ("\\Bbbk") ("\\Bbbl") ("\\Bbbm") ("\\Bbbn") ("\\Bbbo") ("\\Bbbp") ("\\Bbbq") ("\\Bbbr") ("\\Bbbs") ("\\Bbbt") ("\\Bbbu") ("\\Bbbv") ("\\Bbbw") ("\\Bbbx") ("\\Bbby") ("\\Bbbz") ("\\Bbbzero") ("\\Bbbone") ("\\Bbbtwo") ("\\Bbbthree") ("\\Bbbfour") ("\\Bbbfive") ("\\Bbbsix") ("\\Bbbseven") ("\\Bbbeight") ("\\Bbbnine")))
  (if lambdapi-unicode-prefer-company nil (seq-do (function (lambda (com-ltx) (quail-defrule (car com-ltx) (cdr com-ltx)))) (seq-concatenate 'list lambdapi--math-symbol-list-basic lambdapi--math-symbol-list-extended)))
  eval-buffer(#<buffer  *load*-744078> nil "/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-input.el" nil t)  ; Reading at buffer position 7193
  load-with-code-conversion("/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-input.el" "/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-input.el" nil t)
  require(lambdapi-input)
  eval-buffer(#<buffer  *load*> nil "/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-mode.el" nil t)  ; Reading at buffer position 814
  load-with-code-conversion("/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-mode.el" "/home/blanqui/.opam/4.07.1/share/emacs/site-lisp/lambdapi-mode.el" nil t)
  lambdapi-mode()
  set-auto-mode-0(lambdapi-mode nil)
  set-auto-mode()
  normal-mode(t)
  after-find-file(nil t)
  find-file-noselect-1(#<buffer A.lp> "~/src/lambdapi/tmp/A.lp" nil nil "~/src/lambdapi/tmp/A.lp" (560785 2054))
  find-file-noselect("~/src/lambdapi/tmp/A.lp" nil nil t)
  find-file("~/src/lambdapi/tmp/A.lp" t)
  funcall-interactively(find-file "~/src/lambdapi/tmp/A.lp" t)
  call-interactively(find-file nil nil)
  command-execute(find-file)

[fblanqui]

There is no number associated to "\\varsubsetneqq"!

[fblanqui]

Isn't the error in your lambdapi--math-symbol-list-basic or lambdapi--math-symbol-list-extended?

[fblanqui]

In https://github.com/vspinu/math-symbol-lists, it is written:

List of basic LaTeX mathematical symbols. This list maps standard LaTeX math commands to unicode characters. For some symbols in this list the unicode code is missing. It is an extension of LaTeX-math-default' in AucTeX/latex.el, but it doesn't include AMS symbols. See also math-symbol-list-extended' and `math-symbol-list-packages'.

Extended list of mathematical symbols. Each element is a list of the form (CLASS COMMAND UNICODE SYMBOL) where COMMAND is a latex command, UNICODE is the unicode entry point and SYMBOL is the Emacs with the actual unicode character. The last two are equivalent and provided for convenience. This list does not include about 190 of the standard LaTeX math commands in `math-symbol-list-basic' because of the conflicting names between latex and unicode-math standard.

Perhaps you do not properly handle the case where the unicode is missing.

[fblanqui]

By the way, why not including other lists of symbols?

math-symbol-list-packages math-symbol-list-subscripts math-symbol-list-superscripts

[gabrielhdt]

• The problem is that \\varsubsetneqq isn't defined anywhere in math-symbol-lists,
• and yes, we can use the other lists. I'll set that up (at least for subscript and superscript)

[gabrielhdt]

Can you try installing the mode through Melpa? This way we'll be sure you have fresh files and up to date dependencies. \varsubsetneq is defined in math-symbol-list version 1.0 published in 2015...

[fblanqui]

I have version 20151215.1043. But there is also a gnu version 1.2.1 which is marked as obsolete... Should we use https://elpa.gnu.org/packages instead of https://melpa.org/packages/ ?

On http://elpa.gnu.org/packages/math-symbol-lists.html the latest version is math-symbol-lists-1.2.1.el, 2019-May-08.

On https://melpa.org/#/math-symbol-lists the latest version is math-symbol-lists 20200131.2333.

Why do you I have so old versions? What is the difference between elpa.gnu.org and melpa.org? Which one should we use?

Le 19/04/2020 à 13:36, Gabriel Hondet a écrit :

Can you try installing the mode through Melpa? This way we'll be sure you have fresh files and up to date dependencies. |\varsubsetneq| is defined in math-symbol-list version 1.0 published in 2015...

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/lambdapi/issues/362#issuecomment-616111082, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACSZRGPRCMUULGDZIVAHV23RNLO3LANCNFSM4MLJKVKA.

[gabrielhdt]

As far as I understand, ELPA gnu contains a subset of melpa of released packages. MELPA contains the latest versions of packages. If you can, use melpa. Installing lambdapi through melpa should set up everything as needed (there are versions constraints in the package)

[fblanqui]

But I believe that you use the GNU versions, don't you?

Here are the packages I have:

  company-coq        20160126.1550 installed  A collection of extensions for Proof General's Coq mode
  dash-functional    20160615.1351 installed  Collection of useful combinators for Emacs Lisp
  eglot              1.5           installed  Client for Language Server Protocol (LSP) servers
  f                  20161002.800  installed  Modern API for working with files and directories
  flycheck           20170323.614  installed  On-the-fly syntax checking
  gnu-elpa-keyrin... 2019.3        installed  Update Emacs's GPG keyring for GNU ELPA
  math-symbol-lists  20151215.1043 installed  Lists of Unicode math symbols and latex commands
  quickrun           20200315.1029 installed  Run commands quickly
  unicode-fonts      20150826.1532 installed  Configure Unicode fonts
  use-package        20200322.2110 installed  A configuration macro for simplifying your .emacs
  bind-key           20191110.416  dependency A simple way to manage personal keybindings
  company            20160122.1029 dependency Modular text completion framework
  company-math       20160119.548  dependency Completion backends for unicode math symbols and latex tags
  dash               20151216.1315 dependency A modern list library for Emacs
  epl                20150517.433  dependency Emacs Package Library
  flymake            1.0.8         dependency A universal on-the-fly syntax checker
  font-utils         20150806.1051 dependency Utility functions for working with fonts
  jsonrpc            1.0.9         dependency JSON-RPC library
  let-alist          1.0.6         dependency Easily let-bind values of an assoc-list by their names
  list-utils         20160414.702  dependency List-manipulation utility functions
  pcache             20170105.1414 dependency persistent caching for Emacs.
  persistent-soft    20150223.1053 dependency Persistent storage, returning nil on failure
  pkg-info           20150517.443  dependency Information about packages
  s                  20160928.636  dependency The long lost Emacs string manipulation library.
  seq                2.20          dependency Sequence manipulation functions
  ucs-utils          20150826.714  dependency Utilities for Unicode characters
  yasnippet          20160122.1056 dependency Yet another snippet extension for Emacs.

[gabrielhdt]

You need version 1.2.1 of math-symbols-list

[gabrielhdt]

But I see you have use-package, so why don't you try putting

(use-package lambdapi-mode
  :ensure t)

in your init.el?

[fblanqui]

Error (use-package): Failed to install lambdapi-mode: Package ‘lambdapi-mode-’ is unavailable Error (use-package): lambdapi-mode/:catch: Quail key \varsubsetneqq is too long

Le 20/04/2020 à 08:15, Gabriel Hondet a écrit :

But I see you have |use-package|, so why don't you try putting

|(use-package lambdapi-mode :ensure t) |

in your |init.el|?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/lambdapi/issues/362#issuecomment-616334213, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACSZRGPCXNOYMKEUM7N6OUDRNPSBLANCNFSM4MLJKVKA.

[fblanqui]

How can I enforce this?

Le 20/04/2020 à 08:13, Gabriel Hondet a écrit :

You need version 1.2.1 of math-symbols-list

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/lambdapi/issues/362#issuecomment-616333520, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACSZRGLPH5XB57QZG4HKBDLRNPRZ3ANCNFSM4MLJKVKA.

[gabrielhdt]

Have you by any chance input a dash at the end, lambdapi-mode-? Installing with melpa should sort out the dependencies issues. You might have to update your package list with M-x list-packages RET u.

Edit: or better, M-x package-refresh-contents

[fblanqui]

No, I didn't put any dash. And it eems that I can update nothing... :-(

Le 20/04/2020 à 08:55, Gabriel Hondet a écrit :

Have you by any chance input a dash at the end, |lambdapi-mode-|? Installing with melpa should sort out the dependencies issues. You might have to update your package list with |M-x list-packages RET u|.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/Deducteam/lambdapi/issues/362#issuecomment-616348808, or unsubscribe https://github.com/notifications/unsubscribe-auth/ACSZRGJUOPQWSMSAAOXHFU3RNPWUZANCNFSM4MLJKVKA.

[gabrielhdt]

What do you mean you can't update? You can also try using M-x package-delete to remive then reinstall packages

[gabrielhdt]

Can we close this issue, @fblanqui ?