Pseudo-(La)TeX mathematical notation for Racket Scribble docs
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Type Name Latest commit message Commit time
Failed to load latest commit information.
scribblings
.gitignore
LICENSE
README.md
inferrule.rkt
info.rkt
main.rkt
sample.png

README.md

Mathematical notation for Scribble docs

TeXmath is a Racket library for typesetting mathematics in a LaTeX-like syntax.

Example

Logical judgments as rules of inference

#lang scribble/base

@(require texmath)

@inferrule[
      @${e_1 ↝ e_1'}
  ---------------------- "E-App1"
  @${e_1 e_2 ↝ e_1' e_2}
]

@inferrule[
  --------------------------------------- "E-AppAbs"
  @${(λx_11.e_12) v_2 ↝ [x_11↦{}v_2]e_12}
]

@inferrule[
  @${x \fresh}
  ---------------------------- "E-Def"
  @${Σ ⊢ x←v ↝ [x{}↦{}v]Σ ⊢ Ø}
]

@inferrule[
           @${Σ(x) = v}
  ---------------------
  @${Σ,Γ ⊢ x ↝ Σ,Γ ⊢ v}
]

@inferrule[
  @${\{x:T\} ∈ Γ}
  --------------- "T-Var"
  @${<Γ;x>:T}
]

sample output