[Hol-info] Keyboard layout with symbols used in HOL4

[Mario Xerxes Castelán Castro]

This is the custom keyboard layout I use, somewhat similar to the
standard X11 Latin American keyboard layout. It is based on a phonetic
Russian keyboard layout that I made itself based on the standard X11
Latin American keyboard layout.

I am posting it to facilitate other people typing the Unicode symbols
used in HOL4. The instructions to install a custom keyboard layout can
be found with a web search. This layout may require some adaption to
better match your local unadapted keyboard layout instead of the Latin
American one.

// latam2.txt - Keyboard layout for HOL4
//
// Copyright © Mario Castelán Castro.
//
// This work is licensed as free software under the GNU General Public License
// either version 3 or any later version published by the Free Software
// Foundation. See <https://www.gnu.org/licenses/gpl.html>.
//
// As an additional permission (see section 7 of the GNU General Public
// License, version 3) you may convey copies of this work or a work based on
// this work without a copy of the license. The other requirements of the
// license remain in effect. *)

// 
┌─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┬─────┲━━━━━━━━━┓
// │ ` ¬ │ !   │ " ʺ │ # ∗ │ $ λ │ % ε │ &   │ /   │ ( ≼ │ ) ≽ │ = ˚ │ ? ˝ │ \ 
″ ┃Backspace┃
// │ ´ ° │ 1 ¡ │ 2 ʹ │ 3 √ │ 4 ∀ │ 5 ∃ │ 6 ¬ │ 7   │ 8 ≺ │ 9 ≻ │ 0 ≠ │ ' ¿ │ | 
′ ┃    ⌫    ┃
// 
┢━━━━━┷━┱───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┴─┬───┺━┳━━━━━━━┫
// ┃       ┃     │     │     │   Γ │   ∮ │     │   ⋃ │   ⋂ │   ω │   ⊨ │ ” ’ │ 
* × ┃ Enter ┃
// ┃ Tab ↹ ┃ q @ │ w α │ e β │ r γ │ t ∫ │ y ∂ │ u ∪ │ i ∩ │ o Ω │ p ⊢ │ “ ‘ │ 
+ − ┃   ⏎   ┃
// 
┣━━━━━━━┻┱────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┴┬────┺┓
      ┃
// ┃ Caps   ┃     │   ⇎ │   ⇏ │     │     │   𝕌 │   ⊂ │   ∉ │   ≾ │   ≿ │ [ ¨ │ 
] ¯ ┃      ┃
// ┃ Lock ⇬ ┃ a ¬ │ s ⇔ │ d ⇒ │ f ∧ │ g ∨ │ h ∅ │ j ⊆ │ k ∈ │ l — | ñ ~ │ { ^ │ 
} ˇ ┃      ┃
// 
┣━━━━━┳━━┹──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┬──┴──┲━━┷━━━━━┻━━━━━━┫
// ┃Shift┃ > ≥ │   ≲ │   ≳ │   ↔ │   ↦ │     │   ≈ │     │ ; ∙ │ : – │ _ ̣ ┃    
           ┃
// ┃  ⇧  ┃ < ≤ │ z ∏ │ x ∑ │ c ← │ v → │ b ∞ │ n ≡ │ m µ │ , ∘ │ . · | - ˙ ┃    
Shift ⇧    ┃
// 
┗━━━━━┹─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┴─────┺━━━━━━━━━━━━━━━┛

xkb_symbols "latam2" {
    include "latin(type4)"
    name[Group1]="Spanish (Latin American)";

    key <TLDE> {[ dead_acute, dead_grave,   degree,          notsign ]};
    key <AE01> {[         1,     exclam, exclamdown, exclamdown ]};
    key <AE02> {[         2,   quotedbl, U02B9, U02BA ]};
    key <AE03> {[         3, numbersign, U221A, U2217 ]};
    key <AE04> {[         4,     dollar, U2200, Greek_lambda ]};
    key <AE05> {[         5,    percent, U2203, Greek_epsilon ]};
    key <AE08> {[ 8, parenleft, U227A, U227C ]};
    key <AE09> {[ 9, parenright, U227B, U227D ]};
    key <AE10> {[ 0, equals, notequal, dead_abovering ]};
    key <AE11> {[ apostrophe, question,  questiondown, dead_doubleacute]};
    key <AE12> {[ bar, backslash,  minutes, seconds ]};

    key <AD01> {[         q,          Q,           at,           at ]};
    key <AD02> {[         w,          W,        U03B1 ]};
    key <AD03> {[         e,          E,        U03B2 ]};
    key <AD04> {[         r,          R,        U03B3 ]};
    key <AD05> {[         t,          T, U222B, U222E ]};
    key <AD06> {[         y,          Y, U2202 ]};
    key <AD07> {[         u,          U, union, U22C3 ]};
    key <AD08> {[         i,          I, intersection, U22C2 ]};
    key <AD09> {[         o,          O, U03A9, U03C9 ]};
    key <AD10> {[         p,          P, U22A2, U22A8 ]};
    key <AD11> {[ leftdoublequotemark, rightdoublequotemark, 
leftsinglequotemark, rightsinglequotemark ]};
    key <AD12> {[ plus,       asterisk,     U2212,           multiply ]};

    key <AC01> {[         a,          A,  notsign ]};
    key <AC02> {[         s,          S,  ifonlyif, U21CE ]};
    key <AC03> {[         d,          D, implies , U21CF ]};
    key <AC04> {[         f,          F, logicaland ]};
    key <AC05> {[         g,          G, logicalor ]};
    key <AC06> {[         h,          H, U2205, U1D54C ]};
    key <AC07> {[         j,          J,      U2286, includedin ]};
    key <AC08> {[         k,          K,      elementof, U227E ]};
    key <AC09> {[         l,          L,       emdash, U227F ]};
    key <AC10> {[    ntilde,     Ntilde,   asciitilde, asciitilde ]};
    key <AC11> {[ braceleft,  bracketleft,  dead_circumflex, dead_diaeresis ]};
    key <BKSL> {[ braceright, bracketright, dead_caron,      dead_macron ]};

    key <AB01> {[         z,          Z,      U220F, U2272 ]};
    key <AB02> {[         x,          X,      U2211, U2273 ]};
    key <AB03> {[         c,          C, U2190, U2194 ]};
    key <AB04> {[         v,          V, U2192, U21A6 ]};
    key <AB05> {[         b,          B,      U221E ]};
    key <AB06> {[         n,          N,      U2261, U2248 ]};

    key <LSGT> {[ less, greater, lessthanequal, greaterthanequal ]};
    key <AB08> {[ comma, semicolon, U2218, U2219 ]};
    key <AB09> {[ period, colon, periodcentered, endash ]};
    key <AB10> {[ minus, underscore, dead_abovedot, dead_belowdot ]};

    include "level3(ralt_switch)"
};

signature.asc
Description: OpenPGP digital signature

------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info