도움말

코드 블럭

class Functor f where
    fmap :: (a -> b) -> (f a -> f b)

class Functor f => Applicative f where
    pure :: a -> f a
    (<*>) :: f (a -> b) -> f a -> f b

class Applicative m => Monad m where
    (>>=) :: m a -> (a -> m b) -> m b

수식

인라인 스타일 수식을 위해 \(..\)를, 디스플레이 스타일 수식을 위해 \[..\]를 사용한다.

인라인 수식 테스트: \(f(x) = x^2\)

디스플레이 수식 테스트: \[ \newcommand{\type}[2] {#1 \vdash #2 \ \mathrm{type}} \newcommand{\typeeq}[3] {#1 \vdash #2 \equiv #3 \ \mathrm{type}} \newcommand{\term}[3] {#1 \vdash #2 : #3} \newcommand{\termeq}[4] {#1 \vdash #2 \equiv #3 : #4} \begin{array}{l} \type{\Gamma}{A} \\ \typeeq{\Gamma}{A}{B} \\ \term{\Gamma}{M}{A} \\ \termeq{\Gamma}{M}{N}{A} \\ \end{array} \]

증명 나무

MathJax에서 bussproof를 이용해 증명 나무를 그릴 수 있다. \[ \begin{prooftree} \AxiomC{ } \RightLabel{hyp} \UnaryInfC{ $\neg (P \vee \neg P) \vdash \neg (P \vee \neg P)$ } \AxiomC{ } \RightLabel{hyp} \UnaryInfC{ $\neg (P \vee \neg P), P \vdash \neg (P \vee \neg P)$ } \AxiomC{ } \RightLabel{hyp} \UnaryInfC{ $\neg (P \vee \neg P), P \vdash P$ } \RightLabel{ $\vee I_1$ } \UnaryInfC{ $\neg (P \vee \neg P), P \vdash P \vee \neg P$ } \RightLabel{ $\to E$ } \BinaryInfC{ $\neg (P \vee \neg P), P \vdash \bot$ } \RightLabel{ $\to I$ } \UnaryInfC{ $\neg (P \vee \neg P) \vdash \neg P$ } \RightLabel{ $\vee I_2$ } \UnaryInfC{ $\neg (P \vee \neg P) \vdash P \vee \neg P$ } \RightLabel{ $\to E$ } \BinaryInfC{ $\neg (P \vee \neg P) \vdash \bot$ } \RightLabel{ $\to I$ } \UnaryInfC{ $\vdash \neg \neg (P \vee \neg P)$ } \end{prooftree} \]

가환 그림

MathJax에서 amscd 혹은 XyJax를 이용해 가환 그림을 그릴 수 있다.

amscd

\[ \begin{CD} A @>a>> B \\ @VVbV @VVcV \\ C @>d>> D \end{CD} \]

XyJax

\[ \begin{xy} \xymatrix { U \ar@/_/[ddr]_y \ar@{.>}[dr]|{\langle x,y \rangle} \ar@/^/[drr]^x \\ & X \times_Z Y \ar[d]^q \ar[r]_p & X \ar[d]_f \\ & Y \ar[r]^g & Z } \end{xy} \]