# Zulip Chat Archive

## Stream: general

### Topic: Latex

#### Billy Price (Jun 18 2020 at 03:34):

I'm trying to format something in latex - but some unicode characters don't render and some are out of order. I'm rendering with xelatex like this `xelatex --shell-escape file.tex`

.

```
\begin{adjustbox}{max width=\textwidth}
\begin{lstlisting}
inductive proof : context → term → term → Prop
| axm {Γ} {φ} : WF Γ Ω φ → proof Γ φ φ
| vac {Γ} {φ} : WF Γ Ω φ → proof Γ φ ⊤
| abs {Γ} {φ} : WF Γ Ω φ → proof Γ ⊥ φ
| and_intro {Γ} {p q r} : proof Γ p q → proof Γ p r → proof Γ p (q ⋀ r)
| and_left {Γ} (p q r) : proof Γ p (q ⋀ r) → proof Γ p q
| and_right {Γ} (p q r) : proof Γ p (q ⋀ r) → proof Γ p r
| or_intro {Γ} {p q r} : proof Γ p r → proof Γ q r → proof Γ (p ⋁ q) r
| or_left {Γ} (p q r) : proof Γ (p ⋁ q) r → proof Γ p r
| or_right {Γ} (p q r) : proof Γ (p ⋁ q) r → proof Γ q r
| imp_to_and {Γ} {p q r} : proof Γ p (q ⟹ r) → proof Γ (p ⋀ q) r
| and_to_imp {Γ} {p q r} : proof Γ (p ⋀ q) r → proof Γ p (q ⟹ r)
| weakening {Γ} {φ ψ Δ} : proof Γ φ ψ → proof (list.append Γ Δ) φ ψ
| cut {Γ} (φ c ψ) : proof Γ φ c → proof Γ c ψ → proof Γ φ ψ
| all_elim {Γ} {p φ A} : proof Γ p (∀' A φ) → proof (A::Γ) p φ
| all_intro {Γ} {p φ} (A) : proof (A::Γ) p φ → proof Γ p (∀' A φ)
| ex_elim {Γ} {p φ A} : proof Γ p (∃' A φ) → proof (A::Γ) p φ
| ex_intro {Γ} {p φ} (A) : proof (A::Γ) p φ → proof Γ p (∃' A φ)
| extensionality {A} : proof [] ⊤ $ ∀' (𝒫 A) $ ∀' (𝒫 A) $ (∀' A ((𝟘 ∈ 𝟚) ⇔ (𝟘 ∈ 𝟙))) ⟹ (𝟚 ≃[A] 𝟙)
| prop_ext : proof [] ⊤ $ ∀' Ω $ ∀' Ω (𝟙 ⇔ 𝟘) ⟹ (𝟙 ≃[Ω] 𝟘)
| star_unique : proof [] ⊤ $ ∀' Unit (𝟘 ≃[Unit] ⁎)
| pair_exists_rep {A B} : proof [] ⊤ $ ∀' (A ×× B) $ ∃' A $ ∃' B $ 𝟚 ≃[A ×× B] ⟪𝟙,𝟘⟫
| pair_distinct_rep {A B} : proof [] ⊤ $ ∀' A $ ∀' B $ ∀' A $ ∀' B $ (⟪𝟛,𝟙⟫ ≃[A××B] ⟪𝟚,𝟘⟫) ⟹ (𝟛 ≃[A] 𝟚 ⋀ 𝟙 ≃[B] 𝟘)
| sub {Γ} (B) (φ ψ b) : WF Γ B b → proof (B::Γ) φ ψ → proof Γ (⁅φ // b⁆) (⁅ψ // b⁆)
| comp {Γ} (A) (φ) : WF (A::Γ) Ω φ → proof Γ ⊤ (∀' A (𝟘 ∈ ⟦A | φ⟧) ⇔ (⁅φ // 𝟘⁆))
\end{lstlisting}
\end{adjustbox}
```

#### Chris Hughes (Jun 18 2020 at 05:56):

Are you using the lstlean file?

#### Chris Hughes (Jun 18 2020 at 05:58):

There's a list of symbols in that file, if things don't display correctly after using lstlean, then you can add to the list of symbols.

#### Billy Price (Jun 18 2020 at 06:52):

Yes I am. phi is already in that file, and that's the first symbol to not show up

#### Kevin Buzzard (Jun 18 2020 at 06:54):

Those `'`

s are not the best either

#### Billy Price (Jun 18 2020 at 06:58):

In fact I just went back to compiling the sample.tex file provided there and even that's missing unicode symbols. There seems to be no complaint in the log

#### Billy Price (Jun 18 2020 at 06:58):

Actually there is a warning "Package inputenc Warning: inputenc package ignored with utf8 based engines."

#### Billy Price (Jun 18 2020 at 07:08):

Is there a recommended way to compile tex files that use lstlean? I'm using XeLaTeX because I read it was necessary for unicode characters, but I'm realising this might be the problem.

#### Sebastian Ullrich (Jun 18 2020 at 07:53):

IIRC `listings`

has some issues with Unicode even on other Latex engines(?). I always use minted with Luatex for my talks.

```
% https://tex.stackexchange.com/questions/343494/minted-red-box-around-greek-characters
\makeatletter
\AtBeginEnvironment{minted}{\dontdofcolorbox}
\def\dontdofcolorbox{\renewcommand\fcolorbox[4][]{##4}}
\makeatother
```

#### Alexandre Rademaker (Feb 10 2021 at 23:37):

Hi @Sebastian Ullrich , have you use minted with beamer? any sample I can see?

#### Sebastian Ullrich (Feb 11 2021 at 08:24):

@Alexandre Rademaker Nothing beamer-specific, but I recently documented everything I know in https://leanprover.github.io/lean4/doc/syntax_highlight_in_latex.html

Last updated: Aug 03 2023 at 10:10 UTC