EUFA

Liquid Types: Type System and Well-Formedness

Type Well-Formedness

\[\frac{0\le{n}\quad \Gamma;\nu:\langle{n}\rangle_i\vdash{a}}{\Gamma,h\vdash\{\nu:\langle{n}\rangle_i|a\}}\quad[WF-INT]\]



Abstract Block Well-Formedness


    With respect to local environment and preceding indices,

1. no two index bindings overlap, and
2. each type is well-formed

\[
   \frac{
      \begin{aligned}
      {{\Gamma,h}\vdash T}\qquad {Ind(n,T)\cap Dom(b)=\phi}  \\
      {x fresh}\qquad{\Gamma;x:T,h\vdash_Ab[x/@n]}
      \end{aligned}
   }{
      \Gamma, h\vdash_A{n:T,b}
   }
   \quad[WF-FIELD]
\]
\[
   \frac{
      \begin{aligned}
      {\Gamma,h\vdash{T}}\qquad
      {Ind(n^{+m},T)\cap Dom(b)=\phi} \qquad{\Gamma,h\vdash_A{b}}
      \end{aligned}
   }{
      \Gamma, h\vdash_A{n^{+m}:T,b}
   }
   \quad[WF-ARRAY]
\]

在Blogger上使用LaTeX語法 | Using LaTeX on Blogger

利用這篇網誌所教的方法就可以在Blogger (Blogspot)上面成功使用LaTeX的語法了。

此方法使用了一個MathJax套件。這個套件不需要安裝，只需要更改Blogger裡面的頁面範本，讓他可以在讀取blog的時候直接執行一個在該套件伺服器上的javascript就能把網頁裡的LaTeX語句render成數學式子。

Here are some examples of using $\LaTeX$ on Blogger/Blogspot:
$\bullet$Single-line formula: \[P(E) = {n \choose k} p^k (1-p)^{n-k}\]
$\bullet$Inline formula: $BLen(\nu,n)\doteq BS(\nu)=\nu\wedge BE(\nu)=\nu+n$

使用起來就像一般在編輯器裡面輸入一樣，非常方便；而且感覺這個方法應該是可以套用到所有網頁上才對，下次可以試試看。