% This file:
%   http://angg.twu.net/AGDA/Logic2.lagda.tex.html
%   http://angg.twu.net/AGDA/Logic2.lagda.tex
%           (find-angg "AGDA/Logic2.lagda.tex")
% Author: Eduardo Ochs <eduardoochs@gmail.com>
%
% (find-es "agda" "generating-latex")
% (defun e () (interactive) (find-angg "AGDA/Logic2.lagda.tex"))

\documentclass{article}
\usepackage{agda}
\usepackage{fontspec,unicode-math}
\setmainfont{XITS}
\setmathfont{XITS Math}
%\usepackage{newunicodechar}
%\newunicodechar{}{\ensuremath{\mathnormal\lambda}}
\begin{document}



Hello

\begin{code}
module Logic2 where

infix 60 ¬_
infix 30 _∧_
infix 20 _∨_

-- And:
--
data _∧_ (P Q : Set) : Set where
  pair : P → Q → P ∧ Q

proj1 : {P Q : Set} → (P ∧ Q) → P
proj1 {P} {Q} (pair <P> <Q>) = <P>
proj2 : {P Q : Set} → (P ∧ Q) → Q
proj2 {P} {Q} (pair <P> <Q>) = <Q>

-- True:
--
data True : Set where
  tt : True

-- Or:
--
data _∨_ (P Q : Set) : Set where
  ∨-IL : P → P ∨ Q
  ∨-IR : Q → P ∨ Q

inL : {P Q : Set} → P → (P ∨ Q)
inL {P} {Q} <P> = ∨-IL <P>
inR : {P Q : Set} → Q → (P ∨ Q)
inR {P} {Q} <Q> = ∨-IR <Q>

[,] : {P Q R : Set} → (P → R) → (Q → R) → (P ∨ Q → R)
[,] {P} {Q} {R} <P→R> <Q→R> (∨-IL <P>) = <P→R> <P>
[,] {P} {Q} {R} <P→R> <Q→R> (∨-IR <Q>) = <Q→R> <Q>

-- False:
--
data False : Set where

elim-False : {A : Set} → False → A
elim-False ()

-- Not:
--
¬_ : Set → Set
¬ P = P → False

-- Biimplication:
-- ?

-- Exists:
--
data ∃ {A : Set} (P : A → Set) : Set where
  ∃-I : (a : A) → P a → ∃ P

-- Forall:
--
∏ : {A : Set} (P : A → Set) → Set
∏ {A} P = (a : A) → P a
\end{code}

\end{document}





* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
agda --latex Logic2.lagda.tex
laf latex
cd ~/AGDA/latex/
lualatex Logic2.tex

% (find-fline "~/AGDA/latex/")
% (find-fline "~/AGDA/latex/Logic2.tex")



% (find-agdausermanualpage (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualtext (+ 4 195) "4.7 Generating LaTeX")
% (find-agdausermanualpage (+ 4 95) "3.19.3 Literate Agda")
% (find-agdausermanualtext (+ 4 95) "3.19.3 Literate Agda")

% Local Variables:
% coding:  utf-8-unix
% modes:   (latex-mode agda2-mode)
% End: