Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2024type-inferences.tex") % (defun c () (interactive) (find-LATEXsh "lualatex -record 2024type-inferences.tex" :end)) % (defun C () (interactive) (find-LATEXsh "lualatex 2024type-inferences.tex" "Success!!!")) % (defun D () (interactive) (find-pdf-page "~/LATEX/2024type-inferences.pdf")) % (defun d () (interactive) (find-pdftools-page "~/LATEX/2024type-inferences.pdf")) % (defun e () (interactive) (find-LATEX "2024type-inferences.tex")) % (defun o () (interactive) (find-LATEX "2024type-inferences.tex")) % (defun u () (interactive) (find-latex-upload-links "2024type-inferences")) % (defun v () (interactive) (find-2a '(e) '(d))) % (defun d0 () (interactive) (find-ebuffer "2024type-inferences.pdf")) % (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g)) % (code-eec-LATEX "2024type-inferences") % (find-pdf-page "~/LATEX/2024type-inferences.pdf") % (find-sh0 "cp -v ~/LATEX/2024type-inferences.pdf /tmp/") % (find-sh0 "cp -v ~/LATEX/2024type-inferences.pdf /tmp/pen/") % (find-xournalpp "/tmp/2024type-inferences.pdf") % file:///home/edrx/LATEX/2024type-inferences.pdf % file:///tmp/2024type-inferences.pdf % file:///tmp/pen/2024type-inferences.pdf % http://anggtwu.net/LATEX/2024type-inferences.pdf % (find-LATEX "2019.mk") % (find-Deps1-links "Caepro5 Piecewise2 Maxima2") % (find-Deps1-cps "Caepro5 Piecewise2 Maxima2") % (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2") % (find-MM-aula-links "2024type-inferences" "2" "2024tins" "tins") % «.defs» (to "defs") % «.defs-T-and-B» (to "defs-T-and-B") % «.defs-caepro» (to "defs-caepro") % «.defs-pict2e» (to "defs-pict2e") % «.defs-Und2D2» (to "defs-Und2D2") % «.title» (to "title") % «.links» (to "links") % «.instance-Monad-List» (to "instance-Monad-List") \documentclass[oneside,12pt]{article} \usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref") \usepackage{amsmath} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{pict2e} \usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor") \usepackage{colorweb} % (find-es "tex" "colorweb") %\usepackage{tikz} % % (find-dn6 "preamble6.lua" "preamble0") %\usepackage{proof} % For derivation trees ("%:" lines) %\input diagxy % For 2D diagrams ("%D" lines) %\xyoption{curve} % For the ".curve=" feature in 2D diagrams % \usepackage{edrx21} % (find-LATEX "edrx21.sty") \input edrxaccents.tex % (find-LATEX "edrxaccents.tex") \input edrx21chars.tex % (find-LATEX "edrx21chars.tex") \input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex") \input edrxgac2.tex % (find-LATEX "edrxgac2.tex") % % (find-es "tex" "geometry") \usepackage[a6paper, landscape, top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot ]{geometry} % \begin{document} % «defs» (to ".defs") % (find-LATEX "edrx21defs.tex" "colors") % (find-LATEX "edrx21.sty") \def\drafturl{http://anggtwu.net/LATEX/2024-1-C2.pdf} \def\drafturl{http://anggtwu.net/2024.1-C2.html} \def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}} % (find-LATEX "2024-1-C2-carro.tex" "defs-caepro") % (find-LATEX "2024-1-C2-carro.tex" "defs-pict2e") \catcode`\^^J=10 \directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua") % «defs-T-and-B» (to ".defs-T-and-B") \long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}} \def\T(Total: #1 pts){{\bf(Total: #1)}} \def\T(Total: #1 pts){{\bf(Total: #1 pts)}} \def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}} \def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}} % «defs-caepro» (to ".defs-caepro") %L -- dofile "Caepro5.lua" -- (find-angg "LUA/Caepro5.lua" "LaTeX") \def\Caurl #1{\expr{Caurl("#1")}} \def\Cahref#1#2{\href{\Caurl{#1}}{#2}} \def\Ca #1{\Cahref{#1}{#1}} % «defs-pict2e» (to ".defs-pict2e") %L -- dofile "Piecewise2.lua" -- (find-LATEX "Piecewise2.lua") %L --dofile "Escadas1.lua" -- (find-LATEX "Escadas1.lua") \def\pictgridstyle{\color{GrayPale}\linethickness{0.3pt}} \def\pictaxesstyle{\linethickness{0.5pt}} \def\pictnaxesstyle{\color{GrayPale}\linethickness{0.5pt}} \celllower=2.5pt % «defs-Und2D2» (to ".defs-Und2D2") % (tinp 1 "defs-Und2D2") % (tina "defs-Und2D2") %L dofile "Und2D2.lua" -- (find-angg "LUA/Und2D2.lua") \pu \def\und#1#2{\underbrace{#1}_{#2}} % _____ _ _ _ % |_ _(_) |_| | ___ _ __ __ _ __ _ ___ % | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \ % | | | | |_| | __/ | |_) | (_| | (_| | __/ % |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___| % |_| |___/ % % «title» (to ".title") % (2024tinsp 1 "title") % (2024tinsa "title") \thispagestyle{empty} \begin{center} \vspace*{1.2cm} {\bf \Large Some type inferences} \bsk %Some type inferences %\bsk Eduardo Ochs - RCN/PURO/UFF \url{http://anggtwu.net/eev-lean4.html} \end{center} \newpage % «links» (to ".links") % (2024tinsp 2 "links") % (2024tinsa "links") % {\bf Links} % % \scalebox{0.6}{\def\colwidth{9cm}\firstcol{ % }\anothercol{ % }} \newpage % «instance-Monad-List» (to ".instance-Monad-List") % (2024tinsp 2 "instance-Monad-List") % (2024tinsa "instance-Monad-List") % (find-es "lean" "instance-Monad-List") %L bigstr = [=[ %L bind [a1,a2] fun a => bind [b1,b2] fun b => pure (a ,b ) %L -------- --- -------- --- --- --- %L : List A : A : List B : B : A : B %L --------- %L : A×B %L -------------- %L : List A×B %L -------------------------- %L : B → List A×B %L ---------------------------------------- %L : List A×B %L --------------------------------------------------- %L : A → List A×B %L ---------------------------------------------------------------- %L : List A×B %L ]=] %L ut = GrUD.from(bigstr):addallbars():totex_textsf() %L -- ut = GrUD.from(bigstr):addallbars():totex() %L print(ut) %L ut2 = format("\\sa{fig1}{%s}", ut) %L output(ut2) \pu $$\scalebox{0.9}{$ \ga{fig1} $} $$ \newpage %L GrUD.__index.textsfstr = function (grud,str) %L str = str:gsub("[%{%}_]", "\\%1") %L return format("\\textsf{%s}", str) %L end %L bigstr = [=[ %L fun {α β } (ab : α×β) => let (a,_) := ab ; a %L ----- ----------- ----------- ---------- ---- ----------- ------------ ---------- %L "fun" binderIdent binderIdent ? "=>" letDecl? optSemicolon termParser %L ------------------------- ---------- --------------------------------------- %L funImplicitBinder funBinder? termParser? %L ------------------------- %L funBinder %L --------------------------------------------------------------------------------- %L basicFun %L ]=] %L bigstr = [=[ %L fun {α β } (ab : α×β) => let (a , _ ) := ab ; a %L ----- ----------- ----------- --- --- ---- ---- ----- --- ---- ---- ----- ------------ ----- %L "fun" binderIdent binderIdent ident ":" ? "=>" ident "," hole ":=" ident optSemicolon ident %L ------------------------- ------------------- ---------------- %L ImplicitBinder typeAscription tuple %L ------------------------- ------------------- --------------------------- %L funBinder letPatdecl %L --------------------------------------------- -------------------------------------------------- %L basicFun term %L ------------------------------------------------------------------------------------------------------ %L fun %L ]=] %L ut = GrUD.from(bigstr):addallbars():totex_textsf() %L -- ut = GrUD.from(bigstr):addallbars():totex() %L print(ut) %L ut2 = format("\\sa{fig2}{%s}", ut) %L output(ut2) \pu $$\scalebox{0.6}{$ \ga{fig2} $} $$ \GenericWarning{Success:}{Success!!!} % Used by `M-x cv' \end{document} % Local Variables: % coding: utf-8-unix % ee-tla: "tins" % ee-tla: "2024tins" % End: