Path: blob/main/course-contents/notes-formal-02.aux
908 views
\relax
\providecommand\hyper@newdestlabel[2]{}
\providecommand\HyperFirstAtBeginDocument{\AtBeginDocument}
\HyperFirstAtBeginDocument{\ifx\hyper@anchor\@undefined
\global\let\oldnewlabel\newlabel
\gdef\newlabel#1#2{\newlabelxx{#1}#2}
\gdef\newlabelxx#1#2#3#4#5#6{\oldnewlabel{#1}{{#2}{#3}}}
\AtEndDocument{\ifx\hyper@anchor\@undefined
\let\newlabel\oldnewlabel
\fi}
\fi}
\global\let\hyper@last\relax
\gdef\HyperFirstAtBeginDocument#1{#1}
\providecommand\HyField@AuxAddToFields[1]{}
\providecommand\HyField@AuxAddToCoFields[2]{}
\providecommand\BKM@entry[2]{}
\BKM@entry{id=1,dest={73656374696F6E2A2E31},srcline={82}}{5C3337365C3337375C303030415C3030305C3034305C303030645C303030655C303030725C303030695C303030765C303030615C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030615C303030625C3030306F5C303030755C303030745C3030305C3034305C303030725C303030655C3030306E5C303030615C3030306D5C303030695C3030306E5C303030675C3030305C3034305C303030765C303030615C303030725C303030695C303030615C303030625C3030306C5C303030655C30303073}
\BKM@entry{id=2,dest={73656374696F6E2A2E32},srcline={102}}{5C3337365C3337375C303030445C303030655C303030705C303030655C3030306E5C303030645C303030655C3030306E5C303030745C3030305C3034305C303030665C303030755C3030306E5C303030635C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030745C303030795C303030705C303030655C30303073}
\BKM@entry{id=3,dest={73656374696F6E2A2E33},srcline={145}}{5C3337365C3337375C3030305C3133345C303030505C303030695C3030302D5C303030665C3030306F5C303030725C3030306D5C303030615C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030725C303030755C3030306C5C30303065}
\@writefile{toc}{\contentsline {section}{A derivation about renaming variables}{1}{section*.1}\protected@file@percent }
\newlabel{a-derivation-about-renaming-variables}{{}{1}{A derivation about renaming variables}{section*.1}{}}
\@writefile{toc}{\contentsline {section}{Dependent function types}{1}{section*.2}\protected@file@percent }
\newlabel{dependent-function-types}{{}{1}{Dependent function types}{section*.2}{}}
\@writefile{toc}{\contentsline {subsection}{\(\Pi \)-formation rule}{1}{section*.3}\protected@file@percent }
\newlabel{pi-formation-rule}{{}{1}{\texorpdfstring {\(\Pi \)-formation rule}{\textbackslash Pi-formation rule}}{section*.3}{}}
\BKM@entry{id=4,dest={73656374696F6E2A2E34},srcline={163}}{5C3337365C3337375C3030305C3133345C303030505C303030695C3030302D5C303030695C3030306E5C303030745C303030725C3030306F5C303030645C303030755C303030635C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030725C303030755C3030306C5C30303065}
\BKM@entry{id=5,dest={73656374696F6E2A2E35},srcline={188}}{5C3337365C3337375C3030305C3133345C303030505C303030695C3030302D5C303030655C3030306C5C303030695C3030306D5C303030695C3030306E5C303030615C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030725C303030755C3030306C5C30303065}
\BKM@entry{id=6,dest={73656374696F6E2A2E36},srcline={211}}{5C3337365C3337375C3030305C3133345C303030505C303030695C3030302D5C303030635C3030306F5C3030306D5C303030705C303030755C303030745C303030615C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030725C303030755C3030306C5C30303065}
\BKM@entry{id=7,dest={73656374696F6E2A2E37},srcline={233}}{5C3337365C3337375C3030304F5C303030725C303030645C303030695C3030306E5C303030615C303030725C303030795C3030305C3034305C303030665C303030755C3030306E5C303030635C303030745C303030695C3030306F5C3030306E5C3030305C3034305C303030745C303030795C303030705C303030655C30303073}
\@writefile{toc}{\contentsline {subsection}{\(\Pi \)-introduction rule}{2}{section*.4}\protected@file@percent }
\newlabel{pi-introduction-rule}{{}{2}{\texorpdfstring {\(\Pi \)-introduction rule}{\textbackslash Pi-introduction rule}}{section*.4}{}}
\@writefile{toc}{\contentsline {subsection}{\(\Pi \)-elimination rule}{2}{section*.5}\protected@file@percent }
\newlabel{pi-elimination-rule}{{}{2}{\texorpdfstring {\(\Pi \)-elimination rule}{\textbackslash Pi-elimination rule}}{section*.5}{}}
\@writefile{toc}{\contentsline {subsection}{\(\Pi \)-computation rule}{2}{section*.6}\protected@file@percent }
\newlabel{pi-computation-rule}{{}{2}{\texorpdfstring {\(\Pi \)-computation rule}{\textbackslash Pi-computation rule}}{section*.6}{}}
\@writefile{toc}{\contentsline {section}{Ordinary function types}{2}{section*.7}\protected@file@percent }
\newlabel{ordinary-function-types}{{}{2}{Ordinary function types}{section*.7}{}}
\BKM@entry{id=8,dest={73656374696F6E2A2E38},srcline={268}}{5C3337365C3337375C303030435C3030306F5C3030306E5C303030735C303030745C303030725C303030755C303030635C303030745C303030695C3030306F5C3030306E5C3030305C3034305C3030306F5C303030665C3030305C3034305C303030745C303030685C303030655C3030305C3034305C303030695C303030645C303030655C3030306E5C303030745C303030695C303030745C303030795C3030305C3034305C303030665C303030755C3030306E5C303030635C303030745C303030695C3030306F5C3030306E}
\BKM@entry{id=9,dest={73656374696F6E2A2E39},srcline={285}}{5C3337365C3337375C303030435C3030306F5C3030306E5C303030735C303030745C303030725C303030755C303030635C303030745C303030695C3030306F5C3030306E5C3030305C3034305C3030306F5C303030665C3030305C3034305C303030745C303030685C303030655C3030305C3034305C303030635C3030306F5C3030306D5C303030705C3030306F5C303030735C303030695C303030745C303030695C3030306F5C3030306E5C3030305C3034305C3030306F5C303030665C3030305C3034305C303030745C303030775C3030306F5C3030305C3034305C303030665C303030755C3030306E5C303030635C303030745C303030695C3030306F5C3030306E5C30303073}
\@writefile{toc}{\contentsline {subsection}{Construction of the \emph {identity function}}{3}{section*.8}\protected@file@percent }
\newlabel{construction-of-the-identity-function}{{}{3}{\texorpdfstring {Construction of the \emph {identity function}}{Construction of the identity function}}{section*.8}{}}
\@writefile{toc}{\contentsline {subsection}{Construction of the composition of two functions}{3}{section*.9}\protected@file@percent }
\newlabel{construction-of-the-composition-of-two-functions}{{}{3}{Construction of the composition of two functions}{section*.9}{}}
\BKM@entry{id=10,dest={73656374696F6E2A2E3130},srcline={378}}{5C3337365C3337375C303030425C303030695C303030625C3030306C5C303030695C3030306F5C303030675C303030725C303030615C303030705C303030685C30303079}
\BKM@entry{id=11,dest={73656374696F6E2A2E3131},srcline={382}}{5C3337365C3337375C303030425C303030695C303030625C3030306C5C303030695C3030306F5C303030675C303030725C303030615C303030705C303030685C30303079}
\@writefile{toc}{\contentsline {section}{Bibliography}{4}{section*.10}\protected@file@percent }
\newlabel{bibliography}{{}{4}{Bibliography}{section*.10}{}}
\@writefile{toc}{\contentsline {section}{Bibliography}{4}{section*.11}\protected@file@percent }
\newlabel{bibliography-1}{{}{4}{Bibliography}{section*.11}{}}
\gdef \@abspage@last{4}