[Date Prev][Date Next] [Chronological] [Thread] [Top]

AW: [mizar] AW: Mizar Streams

Dear Roman Matuszewski,


the recording software is OBS studio [1], an Open Source recording and streaming software, which is linked to my Twitch account. The editors in use are JEdit (for miz files) and Notepad++ (for abs and voc files). For convenience I attached their edit modes written by me to this file.



Best regards and stay healthy

Sebastian Koch


[1] https://obsproject.com/download

Von: Roman Matuszewski <romat@mizar.org>
Gesendet: Mittwoch, 1. April 2020 21:35:01
An: mizar-forum@mizar.uwb.edu.pl
Cc: Koch, Sebastian
Betreff: Re: [mizar] AW: Mizar Streams
 
Dear Sebastian Koch, thank you for your mail. It is nice to see you
and your Mizar work in live:

https://www.twitch.tv/videos/580708496

Tell me which kind of software you use for that (live work, to see you) ?

Best, Roman Matuszewski


On Wed, 1 Apr 2020, Koch, Sebastian wrote:

> Of course I forgot the link: https://www.twitch.tv/ayutac/
>
> ____________________________________________________________________________________________________________
> Von: owner-mizar-forum@mizar.uwb.edu.pl <owner-mizar-forum@mizar.uwb.edu.pl> im Auftrag von Koch, Sebastian
> <skoch02@students.uni-mainz.de>
> Gesendet: Mittwoch, 1. April 2020 18:24:26
> An: mizar-forum@mizar.uwb.edu.pl
> Betreff: [mizar] Mizar Streams  
>
> Dear Mizar Users,
>
>
> in this time of quarantine I thought of reaching out and stream me writing Mizar articles irregularly. I'm
> probably more likely to stream games or art if you come by at a random time, but some may enjoy it
> nonetheless.
>
>
>
> Best regards
>
> Sebastian Koch
>
>
>
 
<?xml version="1.0"?>

<!DOCTYPE MODE SYSTEM "xmode.dtd">

<MODE>
    <PROPS>
        <PROPERTY NAME="deepIndent" VALUE="false" />
        <PROPERTY NAME="noTabs" VALUE="true" />
        <PROPERTY NAME="indentSize" VALUE="2" />
        <PROPERTY NAME="autoIndent" VALUE="simple" />
        <PROPERTY NAME="wrap" VALUE="hard" />
        <PROPERTY NAME="lineComment" VALUE="::" />
    </PROPS>
    
    <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="TRUE">
        <TERMINATE AT_CHAR="80" />
        <EOL_SPAN TYPE="COMMENT1"><!--T_LINE_START="TRUE"-->::</EOL_SPAN>
        <MARK_PREVIOUS TYPE="LABEL">:</MARK_PREVIOUS>
        <MARK_FOLLOWING TYPE="KEYWORD2" AT_WORD_START="TRUE">$</MARK_FOLLOWING>
        <SEQ TYPE="KEYWORD3" AT_WHITESPACE_END="TRUE">set</SEQ>
            
        <!-- KEYWORD1 are basic constructs -->
        <!-- KEYWORD2 are mode, func etc. -->
        <!-- KEYWORD3 are logical connections and mathematical quantifiers -->
        <!-- KEYWORD4 are type quantifiers of some kind -->
        <!-- "the", "non" and "@proof" weren't forgotten but chosen not to be highlighted --> 
        <!-- on the other hand, "in" was chosen to be marked -->
        <KEYWORDS>
          <KEYWORD1>environ</KEYWORD1>
          <KEYWORD1>vocabularies</KEYWORD1>
          <KEYWORD1>notations</KEYWORD1>
          <KEYWORD1>constructors</KEYWORD1>
          <KEYWORD1>registrations</KEYWORD1>
          <KEYWORD1>definitions</KEYWORD1>
          <KEYWORD1>theorems</KEYWORD1>
          <KEYWORD1>schemes</KEYWORD1>
          <KEYWORD1>requirements</KEYWORD1>
          <KEYWORD1>expansions</KEYWORD1>
          <KEYWORD1>equalities</KEYWORD1>
          <KEYWORD1>begin</KEYWORD1>
          <KEYWORD1>reserve</KEYWORD1>
          <KEYWORD1>definition</KEYWORD1>
          <KEYWORD1>end</KEYWORD1>
          <KEYWORD1>redefine</KEYWORD1>
          <KEYWORD1>registration</KEYWORD1>
          <KEYWORD1>cluster</KEYWORD1>
          <KEYWORD1>notation</KEYWORD1>
          <KEYWORD1>canceled</KEYWORD1>
          <KEYWORD1>identify</KEYWORD1>
          <KEYWORD1>correctness</KEYWORD1>
          <KEYWORD1>existence</KEYWORD1>
          <KEYWORD1>uniqueness</KEYWORD1>
          <KEYWORD1>coherence</KEYWORD1>
          <KEYWORD1>compatibility</KEYWORD1>
          <KEYWORD1>consistency</KEYWORD1>
          <KEYWORD1>theorem</KEYWORD1>
          <KEYWORD1>scheme</KEYWORD1>
          <KEYWORD1>provided</KEYWORD1>
          <KEYWORD1>proof</KEYWORD1>
        
          <KEYWORD1>struct</KEYWORD1>
          <KEYWORD1>mode</KEYWORD1>
          <KEYWORD1>func</KEYWORD1>
          <KEYWORD1>pred</KEYWORD1>
          <KEYWORD1>attr</KEYWORD1>
          <KEYWORD1>deffunc</KEYWORD1>
          <KEYWORD1>defpred</KEYWORD1>
          <KEYWORD1>it</KEYWORD1>
        
          <KEYWORD1>synonym</KEYWORD1>
          <KEYWORD1>antonym</KEYWORD1>
          <KEYWORD1>commutativity</KEYWORD1>
          <KEYWORD1>idempotence</KEYWORD1>
          <KEYWORD1>involutiveness</KEYWORD1>
          <KEYWORD1>projectivity</KEYWORD1>
          <KEYWORD1>symmetry</KEYWORD1>
          <KEYWORD1>asymmetry</KEYWORD1>
          <KEYWORD1>connectedness</KEYWORD1>
          <KEYWORD1>reflexivity</KEYWORD1>
          <KEYWORD1>irreflexivity</KEYWORD1>
        
          <KEYWORD2>thus</KEYWORD2>
          <KEYWORD2>hence</KEYWORD2>
          <KEYWORD2>hereby</KEYWORD2>
          <KEYWORD2>thesis</KEYWORD2>
          <KEYWORD2>contradiction</KEYWORD2>
        
          <!--<KEYWORD4>(?&lt;=\s|&#13;|&#10;reserve.*)for</KEYWORD4>
          <KEYWORD4>(?&lt;=\s|&#13;|&#10;cluster.*)for</KEYWORD4>
          <KEYWORD4>(?&lt;=\s|&#13;|&#10;synonym.*)for</KEYWORD4>
          <KEYWORD4>(?&lt;=\s|&#13;|&#10;antonym.*)for</KEYWORD4>-->
        
          <KEYWORD2>let</KEYWORD2>
          <KEYWORD2>such</KEYWORD2>
          <KEYWORD2>that</KEYWORD2>
          <KEYWORD3>if</KEYWORD3>
          <KEYWORD3>otherwise</KEYWORD3>
          <KEYWORD2>when</KEYWORD2>
          <KEYWORD2>and</KEYWORD2>
          <!--<KEYWORD2>per cases</KEYWORD2>-->
        
          <KEYWORD3>&amp;</KEYWORD3>
          <KEYWORD3>or</KEYWORD3>
          <KEYWORD3>implies</KEYWORD3>
          <KEYWORD3>iff</KEYWORD3>
          <KEYWORD3>not</KEYWORD3>
          <KEYWORD3>for</KEYWORD3>
          <KEYWORD3>holds</KEYWORD3>
          <KEYWORD3>ex</KEYWORD3>
          <KEYWORD3>st</KEYWORD3>
          <KEYWORD2>per cases</KEYWORD2>
          <KEYWORD2>case</KEYWORD2>
          <KEYWORD2>suppose</KEYWORD2>
          <KEYWORD2>assume</KEYWORD2>
          <KEYWORD2>given</KEYWORD2>
          <KEYWORD2>consider</KEYWORD2>
          <KEYWORD2>reconsider</KEYWORD2>
          <KEYWORD2>take</KEYWORD2>
        
          <KEYWORD2>now</KEYWORD2>
          <KEYWORD2>then</KEYWORD2>
          <KEYWORD2>by</KEYWORD2>
          <KEYWORD2>from</KEYWORD2>
        
          <KEYWORD4>being</KEYWORD4>
          <KEYWORD4>be</KEYWORD4>
          <KEYWORD4>over</KEYWORD4>
          <!--<KEYWORD4>(?&lt;=\s|&#13;|&#10;cluster.*)-></KEYWORD4>-->
          <!--<KEYWORD4>of</KEYWORD4>-->
          <KEYWORD4>is</KEYWORD4>
          <KEYWORD4>as</KEYWORD4>
          <KEYWORD4>means</KEYWORD4>
          <KEYWORD4>equals</KEYWORD4>
          <KEYWORD4>with</KEYWORD4>
          <KEYWORD4>qua</KEYWORD4>
          <KEYWORD4>in</KEYWORD4>
          <KEYWORD4>where</KEYWORD4>
        </KEYWORDS>
        
    </RULES>
</MODE>

<NotepadPlus>
    <UserLang name="Mizar" ext="" udlVersion="2.1">
        <Settings>
            <Global caseIgnored="no" allowFoldOfComments="no" foldCompact="no" forcePureLC="0" decimalSeparator="0" />
            <Prefix Keywords1="no" Keywords2="no" Keywords3="no" Keywords4="no" Keywords5="no" Keywords6="no" Keywords7="no" Keywords8="no" />
        </Settings>
        <KeywordLists>
            <Keywords name="Comments">00:: 01 02 03:Def 04:</Keywords>
            <Keywords name="Numbers, prefix1"></Keywords>
            <Keywords name="Numbers, prefix2"></Keywords>
            <Keywords name="Numbers, extras1"></Keywords>
            <Keywords name="Numbers, extras2"></Keywords>
            <Keywords name="Numbers, suffix1"></Keywords>
            <Keywords name="Numbers, suffix2"></Keywords>
            <Keywords name="Numbers, range"></Keywords>
            <Keywords name="Operators1"></Keywords>
            <Keywords name="Operators2"></Keywords>
            <Keywords name="Folders in code1, open">proof</Keywords>
            <Keywords name="Folders in code1, middle"></Keywords>
            <Keywords name="Folders in code1, close">end;</Keywords>
            <Keywords name="Folders in code2, open"></Keywords>
            <Keywords name="Folders in code2, middle"></Keywords>
            <Keywords name="Folders in code2, close"></Keywords>
            <Keywords name="Folders in comment, open"></Keywords>
            <Keywords name="Folders in comment, middle"></Keywords>
            <Keywords name="Folders in comment, close"></Keywords>
            <Keywords name="Keywords1">environ&#x000D;&#x000A;vocabularies&#x000D;&#x000A;notations&#x000D;&#x000A;qua&#x000D;&#x000A;pred&#x000D;&#x000A;it&#x000D;&#x000A;constructors&#x000D;&#x000A;registrations&#x000D;&#x000A;definitions&#x000D;&#x000A;equalities&#x000D;&#x000A;requirements&#x000D;&#x000A;registrations&#x000D;&#x000A;theorems&#x000D;&#x000A;schemes&#x000D;&#x000A;begin&#x000D;&#x000A;theorem&#x000D;&#x000A;proof&#x000D;&#x000A;end&#x000D;&#x000A;definition&#x000D;&#x000A;registration&#x000D;&#x000A;cluster&#x000D;&#x000A;existence&#x000D;&#x000A;existence;&#x000D;&#x000A;uniqueness&#x000D;&#x000A;uniqueness;&#x000D;&#x000A;coherence&#x000D;&#x000A;coherence;&#x000D;&#x000A;correctness&#x000D;&#x000A;correctness;&#x000D;&#x000A;compatibility&#x000D;&#x000A;compatibility;&#x000D;&#x000A;reflexivity&#x000D;&#x000A;reflexivity;&#x000D;&#x000A;symmetry&#x000D;&#x000A;symmetry;&#x000D;&#x000A;irreflexivity&#x000D;&#x000A;irreflexivity;&#x000D;&#x000A;reducibility&#x000D;&#x000A;reducibility;&#x000D;&#x000A;idempotence&#x000D;&#x000A;idempotence;&#x000D;&#x000A;involutiveness&#x000D;&#x000A;involutiveness;&#x000D;&#x000A;identify&#x000D;&#x000A;with&#x000D;&#x000A;canceled&#x000D;&#x000A;canceled;&#x000D;&#x000A;provided&#x000D;&#x000A;redefine&#x000D;&#x000A;scheme&#x000D;&#x000A;func&#x000D;&#x000A;attr&#x000D;&#x000A;mode&#x000D;&#x000A;reserve&#x000D;&#x000A;equals&#x000D;&#x000A;means&#x000D;&#x000A;if&#x000D;&#x000A;otherwise&#x000D;&#x000A;reflexivity&#x000D;&#x000A;struct&#x000D;&#x000A;notation&#x000D;&#x000A;synonym&#x000D;&#x000A;antonym&#x000D;&#x000A;reduce&#x000D;&#x000A;to&#x000D;&#x000A;defpred&#x000D;&#x000A;deffunc&#x000D;&#x000A;-&gt;</Keywords>
            <Keywords name="Keywords2">let&#x000D;&#x000A;consider&#x000D;&#x000A;reconsider&#x000D;&#x000A;take&#x000D;&#x000A;thus&#x000D;&#x000A;hence&#x000D;&#x000A;thesis&#x000D;&#x000A;then&#x000D;&#x000A;such&#x000D;&#x000A;that&#x000D;&#x000A;contradiction&#x000D;&#x000A;contradiction;&#x000D;&#x000A;per&#x000D;&#x000A;cases&#x000D;&#x000A;suppose&#x000D;&#x000A;by&#x000D;&#x000A;from&#x000D;&#x000A;now&#x000D;&#x000A;hereby&#x000D;&#x000A;assume&#x000D;&#x000A;thesis;</Keywords>
            <Keywords name="Keywords3">be&#x000D;&#x000A;being&#x000D;&#x000A;is&#x000D;&#x000A;of&#x000D;&#x000A;set</Keywords>
            <Keywords name="Keywords4">non</Keywords>
            <Keywords name="Keywords5">&#x000D;&#x000A;for&#x000D;&#x000A;iff&#x000D;&#x000A;implies&#x000D;&#x000A;ex&#x000D;&#x000A;st&#x000D;&#x000A;holds&#x000D;&#x000A;&amp;&#x000D;&#x000A;or&#x000D;&#x000A;not</Keywords>
            <Keywords name="Keywords6"></Keywords>
            <Keywords name="Keywords7"></Keywords>
            <Keywords name="Keywords8"></Keywords>
            <Keywords name="Delimiters"></Keywords>
        </KeywordLists>
        <Styles>
            <WordsStyle name="DEFAULT" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="COMMENTS" fgColor="008000" bgColor="FFFFFF" fontName="" fontStyle="2" nesting="0" />
            <WordsStyle name="LINE COMMENTS" fgColor="800080" bgColor="FFFFFF" fontName="" fontStyle="2" nesting="0" />
            <WordsStyle name="NUMBERS" fgColor="008000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="KEYWORDS1" fgColor="0000A0" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
            <WordsStyle name="KEYWORDS2" fgColor="005900" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
            <WordsStyle name="KEYWORDS3" fgColor="808040" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="KEYWORDS4" fgColor="400000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="KEYWORDS5" fgColor="00AA00" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
            <WordsStyle name="KEYWORDS6" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="KEYWORDS7" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="KEYWORDS8" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="OPERATORS" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="FOLDER IN CODE1" fgColor="0000A0" bgColor="FFFFFF" fontName="" fontStyle="1" nesting="0" />
            <WordsStyle name="FOLDER IN CODE2" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="FOLDER IN COMMENT" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS1" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS2" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS3" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS4" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS5" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS6" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS7" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
            <WordsStyle name="DELIMITERS8" fgColor="000000" bgColor="FFFFFF" fontName="" fontStyle="0" nesting="0" />
        </Styles>
    </UserLang>
</NotepadPlus>