Group theory Merge Conflict Resolution

Reference Manual/.latexmkrc

@@ -0,0 +1,3 @@
+$pdflatex = "xelatex %O %S";
+$pdf_mode = 1;
+$dvi_mode = $postscript_mode = 0;

Reference Manual/lisa.tex

@@ -1,68 +1,63 @@
+% !TEX program = xelatex
 \documentclass[11pt,a4paper]{book}
-\usepackage[utf8]{inputenc}
-\usepackage[english]{babel}
-\usepackage{amsmath}
-\usepackage{amsfonts}
-\usepackage{amssymb}
-\usepackage{listings}
-\usepackage{amsthm}
-\usepackage{csquotes}
-\usepackage[strings]{underscore}
-\usepackage{url}
-\usepackage{bussproofs}
-\usepackage{makecell}
-
-
-\newtheorem{thm}{Theorem}
-\newtheorem{lemma}{Lemma}
-\newtheorem{corollary}{Corollary}
-\theoremstyle{definition}
-\newtheorem{defin}{Definition}
-\newtheorem{ex}{Example}
-
-\newtheorem{axz}{}
-\renewcommand\theaxz{Z\arabic{axz}}
-\newtheorem{axzf}{}
-\renewcommand\theaxzf{ZF\arabic{axzf}}
-\newtheorem{axtg}{}
-\renewcommand\theaxtg{TG\arabic{axtg}}
-
-\lstset{
-language=Scala,
-escapeinside={(*@}{@*)}
-}
-
-%\lstdefinelanguage{scala}{
-%  alsoletter={@,=,>},
-%  morekeywords={abstract, case, class, def, do, Input, Output, then,
-%        else, extends, false, free, if, implicit, match,
-%        object, true, val, var, while, sealed, or, given,
-%        for, dependent, null, type, with, try, catch, finally,
-%        import, final, return, new, override, this, trait,
-%        private, public, protected, package, throw, using},
-%  sensitive=true,  
-%  morecomment=[l]{//},
-%  morecomment=[s]{/*}{*/},
-%  morestring=[b]",  
-%}
-%\lstset{mathescape,escapeinside={!*}{*!},columns=fullflexible,morekeywords={if,then,else,return,match,with,end,let,in, data, type, :=, def}}
-
 
+\input{macro}
+\input{shortcuts} 
 
 \title{LISA Reference Manual (WIP)}
 \author{Simon Guilloud\\Laboratory for Automated Reasoning and Analysis, EPFL}
 \date{}
 
 \begin{document}
-\maketitle
+
+\newfontfamily\titlefont{Arial}
+
+\begin{titlepage}
+\titlefont 
+%\fontfamily{\sfdefault}\selectfont
+
+    \begin{center}
+        \vspace*{1cm}
+
+        \textbf{\Huge LISA Reference Manual}
+
+        \vspace{1.5cm}
+
+        \textbf{\large WIP Edition}
+
+        \vspace{1.5cm}
+
+        {\Large Laboratory for Automated Reasoning and Analysis, EPFL, Switzerland}
+
+        \vspace{1.5cm}
+
+        \date{}
+
+    \end{center}
+    \vspace*{10em}
+    \begin{flushright}\huge
+        \begin{tabular}{l}
+         Contributors: \hspace*{2em} \\[1em]
+         Simon Guilloud\\
+         Sankalp Gambhir
+        \end{tabular}
+    \end{flushright}
+
+ \end{titlepage}
 \chapter*{Introduction}
 
-This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations \cite{DBLP:conf/tacas/GuilloudK22}.
+This document aims to give a complete documentation on LISA. Tentatively, every chapter and section will explain a part or concept of LISA, and explains both its implementation and its theoretical foundations. 
+
+\tableofcontents
+
+\input{kernel.tex}
+
+\input{prooflib.tex}
 
-\input{part1.tex}
+\input{theory.tex}
 
-\input{part2.tex}
+\input{theorytopics.tex}
 
 \bibliographystyle{plain}
-\bibliography{biblio.bib}
+\bibliography{sguilloud.bib}
 \end{document}

Reference Manual/macro.tex

@@ -0,0 +1,119 @@
+% macro.tex
+
+\usepackage[utf8]{inputenc}
+\usepackage{url}
+\usepackage{graphicx}
+\usepackage[english]{babel}
+\usepackage{amsmath}
+\usepackage{amsfonts}
+\usepackage{amssymb}
+\usepackage{amsthm}
+\usepackage{listings}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{csquotes}
+\usepackage[strings]{underscore}
+\usepackage{hyperref}
+\usepackage{bussproofs}
+\usepackage{makecell}
+\usepackage{subcaption}
+\usepackage[dvipsnames]{xcolor}
+\usepackage{float}
+\usepackage{xspace}
+\usepackage[ruled,vlined]{algorithm2e}
+\usepackage{array}
+\usepackage{arial}
+\usepackage[T1]{fontenc}
+\renewcommand\sfdefault{ua1}
+\sloppy % better (?) margin handling
+
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}
+\newtheorem{corollary}{Corollary}
+
+\newtheorem{axz}{}
+\renewcommand\theaxz{Z\arabic{axz}}
+\newtheorem{axzf}{}
+\renewcommand\theaxzf{ZF\arabic{axzf}}
+\newtheorem{axtg}{}
+\renewcommand\theaxtg{TG\arabic{axtg}}
+
+\theoremstyle{definition}
+\newtheorem{definition}{Definition}
+\newtheorem{example}{Example}
+\newcommand*{\definitionautorefname}{Definition}
+
+
+
+%Code
+%\usepackage[nomap]{FiraMono} 
+\usepackage{fontspec}
+\setmonofont[
+  Contextuals={Alternate}
+]{Fira Code}
+
+\makeatletter
+\def\verbatim@nolig@list{}
+\makeatother
+
+\definecolor{green}{rgb}{0, 0.6, 0}
+
+\definecolor{comments}{RGB}{80,0,110}
+
+\lstdefinelanguage{scala}{
+    alsoletter={@,=,>},
+    keywordstyle = {\color{blue}},
+    keywordstyle = [2]{\color{blue}},
+    commentstyle = \color{comments},
+    morekeywords = [2]{abstract, case, class, def, do, Input, Output, then,
+        else, extends, false, free, if, implicit, match,
+        object, true, val, var, while, sealed, or,
+        for, dependent, null, type, with, try, catch, finally,
+        import, final, return, new, override, this, trait,
+        private, public, protected, package, throw},
+    sensitive = true, 
+    %numbers=left,
+    stepnumber=1,
+    morecomment = [l]{//},
+    morecomment = [s]{/*}{*/},
+    morestring = [b]",  
+    otherkeywords = {;,<<,>>,++},
+}
+
+\lstdefinelanguage{lisa}{
+    alsoletter={@,=,>},
+    keywordstyle = {\color{blue}},
+    keywordstyle = [2]{\color{blue}},
+    keywordstyle = [3]{\color{green}},
+    keywordstyle = [4]{\color{teal}},
+    commentstyle = \color{comments},
+    morekeywords = [2]{abstract, case, class, def, do, Input, Output, then,
+        else, extends, false, free, if, implicit, match,
+        object, true, val, var, while, sealed, or,
+        for, dependent, null, type, with, try, catch, finally,
+        import, final, return, new, override, this, trait,
+        private, public, protected, package, throw, given},
+    morekeywords = [3]{have, andThen, thenHave, Theorem, by, DEF, The, Lemma, subproof, assume},
+    sensitive = true, 
+    numbers=left,
+    stepnumber=1,
+    morecomment = [l]{//},
+    morecomment = [s]{/*}{*/},
+    morestring = [b]",  
+    otherkeywords = {;,<<,>>,++},
+}
+
+
+
+\definecolor{verylightgray}{rgb}{0.96, 0.94, 0.92}
+\lstset{
+    backgroundcolor = \color{verylightgray},
+    basicstyle=\footnotesize\linespread{1.15}\ttfamily,
+    mathescape,
+    escapeinside={!*}{*!},
+    columns=fullflexible,
+    morekeywords={if,then,else,return,match,with,end,let,in, data, type, :=, def}
+}
+
+\DeclareMathOperator{\pick}{pick}
+