diff --git a/_posts/read_sf_lf/2019-01-01-sf-lf-01-basics.md b/_posts/read_sf_lf/2019-01-01-sf-lf-01-basics.md
index 10d585b3cdf..7511ff4adb3 100644
--- a/_posts/read_sf_lf/2019-01-01-sf-lf-01-basics.md
+++ b/_posts/read_sf_lf/2019-01-01-sf-lf-01-basics.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」1 Basics"
+title: "「SF-LC」1 Basics"
 subtitle: "Logical Foundations - Functional Programming in Coq"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-02-sf-lf-02-induction.md b/_posts/read_sf_lf/2019-01-02-sf-lf-02-induction.md
index a45d5a60402..071482cdad6 100644
--- a/_posts/read_sf_lf/2019-01-02-sf-lf-02-induction.md
+++ b/_posts/read_sf_lf/2019-01-02-sf-lf-02-induction.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」2 Induction"
+title: "「SF-LC」2 Induction"
 subtitle: "Logical Foundations - Proof by Induction"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-03-sf-lf-03-list.md b/_posts/read_sf_lf/2019-01-03-sf-lf-03-list.md
index e0c8640a4e3..096c5efc64b 100644
--- a/_posts/read_sf_lf/2019-01-03-sf-lf-03-list.md
+++ b/_posts/read_sf_lf/2019-01-03-sf-lf-03-list.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」3 List"
+title: "「SF-LC」3 List"
 subtitle: "Logical Foundations - Working with Structured Data"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
@@ -15,13 +15,15 @@ tags:
 Pair of Numbers
 ---------------
 
-Q: Why it's also called `inductive`? Is it just a keyword or ..
-A: No. Inductive only means _building things bottom-up_, it doesn't have to reference itself.
+Q: Why name `inductive`? 
+A: Inductive means _building things bottom-up_, it doesn't have to self-referencial (recursive)
 (see below `induction on lists` as well.)
 
 ```coq
 Inductive natprod : Type :=
   | pair (n1 n2 : nat).
+
+Notation "( x , y )" := (pair x y).
 ```
 
 Proof on pair cannot simply `simpl.`
@@ -57,7 +59,7 @@ It only generate **one subgoal**, becasue
 
 The **prove by case analysis (exhaustive)** is just an application of the idea of _destruction_! 
 
-the idea simply _destruct_ the data type into its data constructors (representing ways of construct this data)
+the idea simply _destruct_ the data type into its data constructors (representing ways of constructing this data)
 
 - Java class has only 1 way to construct (via its constructor)
 - Scala case class then have multiple way to construct
diff --git a/_posts/read_sf_lf/2019-01-04-sf-lf-04-poly.md b/_posts/read_sf_lf/2019-01-04-sf-lf-04-poly.md
index 30455600e6a..79aa54de477 100644
--- a/_posts/read_sf_lf/2019-01-04-sf-lf-04-poly.md
+++ b/_posts/read_sf_lf/2019-01-04-sf-lf-04-poly.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」4 Poly"
+title: "「SF-LC」4 Poly"
 subtitle: "Logical Foundations - Polymorphism and Higher-Order Functions"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-05-sf-lf-05-tactics.md b/_posts/read_sf_lf/2019-01-05-sf-lf-05-tactics.md
index 7546b8ef9d7..d77a8921e27 100644
--- a/_posts/read_sf_lf/2019-01-05-sf-lf-05-tactics.md
+++ b/_posts/read_sf_lf/2019-01-05-sf-lf-05-tactics.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」5 Tactics"
+title: "「SF-LC」5 Tactics"
 subtitle: "Logical Foundations - More Basic Tactics"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-06-sf-lf-06-logic.md b/_posts/read_sf_lf/2019-01-06-sf-lf-06-logic.md
index 1acaba52c2a..32a7355d099 100644
--- a/_posts/read_sf_lf/2019-01-06-sf-lf-06-logic.md
+++ b/_posts/read_sf_lf/2019-01-06-sf-lf-06-logic.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」6 Logic"
+title: "「SF-LC」6 Logic"
 subtitle: "Logical Foundations - Logic in Coq"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
@@ -21,7 +21,8 @@ We have seen...
 * _proofs_: ways of presenting __evidence__ for the truth of a proposition
 
 
-## `Prop` type
+`Prop` type
+-----------
 
 ```coq
 Check 3 = 3.  (* ===> Prop. A provable prop *)
@@ -60,7 +61,8 @@ Check @eq. (* ===> forall A : Type, A -> A -> Prop *)
 Theroems are types, and proofs are existentials.
 
 
-## Slide Q&A - 1.
+Slide Q&A - 1.
+--------------
 
 1. `Prop`
 2. `Prop`
@@ -82,7 +84,8 @@ Definition foo : (forall n:nat, bool) (* foo: nat -> bool *)
 ```
 
 
-## Logical Connectives
+Logical Connectives
+-------------------
 
 > noticed that connectives symbols are "unicodize" in book and spacemacs.
 
diff --git a/_posts/read_sf_lf/2019-01-07-sf-lf-07-indprop.md b/_posts/read_sf_lf/2019-01-07-sf-lf-07-indprop.md
index bea6d658065..8d37b787015 100644
--- a/_posts/read_sf_lf/2019-01-07-sf-lf-07-indprop.md
+++ b/_posts/read_sf_lf/2019-01-07-sf-lf-07-indprop.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」7 Ind Prop"
+title: "「SF-LC」7 Ind Prop"
 subtitle: "Logical Foundations - Inductively Defined Propositions (归纳定义命题)"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-08-sf-lf-08-map.md b/_posts/read_sf_lf/2019-01-08-sf-lf-08-map.md
index cd55643ff97..cf2489cdcb2 100644
--- a/_posts/read_sf_lf/2019-01-08-sf-lf-08-map.md
+++ b/_posts/read_sf_lf/2019-01-08-sf-lf-08-map.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」8 Maps"
+title: "「SF-LC」8 Maps"
 subtitle: "Logical Foundations - Total and Partial Maps"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-09-sf-lf-09-proof-object.md b/_posts/read_sf_lf/2019-01-09-sf-lf-09-proof-object.md
index 708bb825ee0..511076bc06b 100644
--- a/_posts/read_sf_lf/2019-01-09-sf-lf-09-proof-object.md
+++ b/_posts/read_sf_lf/2019-01-09-sf-lf-09-proof-object.md
@@ -1,21 +1,17 @@
 ---
-title: "「逻辑基础」9 ProofObjects"
+title: "「SF-LC」9 ProofObjects"
 subtitle: "Logical Foundations - The Curry-Howard Correspondence "
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
 
-## Props as Types
-
-## Top
-
 > "Algorithms are the computational content of proofs." —Robert Harper
 
 So the book material is designed to be gradually reveal the facts that 
@@ -36,7 +32,8 @@ e.g.
 > Proving manipulates evidence, much as programs manipuate data.
 
 
-## Curry-Howard Correspondence
+Curry-Howard Correspondence
+---------------------------
 
 > deep connection between the world of logic and the world of computation:
 
@@ -51,8 +48,11 @@ e.g.
 `ev_SS : ∀n, even n -> even (S (S n))`
 - takes a nat `n` and evidence for `even n` and yields evidence for `even (S (S n))`.
 
+This is _Props as Types_.
 
-## Proof Objects
+
+Proof Objects
+-------------
 
 Proofs are data! We can see the _proof object_ that results from this _proof script_.
 
@@ -60,7 +60,6 @@ Proofs are data! We can see the _proof object_ that results from this _proof scr
 Print ev_4.
 (* ===> ev_4 = ev_SS 2 (ev_SS 0 ev_0) 
              : even 4  *)
-             
 
 Check (ev_SS 2 (ev_SS 0 ev_0)).     (* concrete derivation tree, we r explicitly say the number tho *)
 (* ===> even 4 *)
@@ -69,7 +68,8 @@ Check (ev_SS 2 (ev_SS 0 ev_0)).     (* concrete derivation tree, we r explicitly
 These two ways are the same in principle!
 
 
-## Proof Scripts
+Proof Scripts
+-------------
 
 `Show Proof.`  will show the _partially constructed_ proof terms / objects.
 `?Goal` is the _unification variable_. (the hold we need to fill in to complete the proof)
@@ -96,7 +96,8 @@ Qed.
 Agda doesn't have tactics built-in. (but also Interactive)
 
 
-## Quantifiers, Implications, Functions
+Quantifiers, Implications, Functions
+------------------------------------
 
 In Coq's _computational universe_ (where data structures and programs live), to give `->`:
 - constructors (introduced by `Indutive`)
@@ -147,11 +148,10 @@ Now we call them `dependent type function`
 
 
 
-
 ### `→` is degenerated `∀` (`Pi`)
 
-> Notice that both implication (→) and quantification (∀) correspond to functions on evidence. 
-> In fact, they are really the same thing: → is just a shorthand for a degenerate use of ∀ where there is no dependency, i.e., no need to give a name to the type on the left-hand side of the arrow:
+> Notice that both implication (`→`) and quantification (`∀`) correspond to functions on evidence. 
+> In fact, they are really the same thing: `→` is just a shorthand for a degenerate use of `∀` where there is no dependency, i.e., no need to give a name to the type on the left-hand side of the arrow:
 
 ```coq
   ∀(x:nat), nat 
@@ -164,17 +164,20 @@ Now we call them `dependent type function`
 ```
 
 > In general, `P → Q` is just syntactic sugar for `∀ (_:P), Q`.
-Same as what TAPL mentioned for `Pi`.
 
+TaPL also mention this fact for `Pi`.
 
-## Q&A - Slide 15
+
+Q&A - Slide 15
+--------------
 
 1. `∀ n, even n → even (4 + n)`. (`2 + n = S (S n)`)
 
 
 
 
-## Programming with Tactics.
+Programming with Tactics.
+-------------------------
 
 If we can build proofs by giving explicit terms rather than executing tactic scripts, 
 you may be wondering whether we can _build programs using tactics_? Yes!
@@ -234,7 +237,8 @@ Unlike Agda - you program intensively in dependent type...?
 When Extracting to OCaml...Coq did a lot of `Object.magic` for coercion to bypass OCaml type system. (Coq has maken sure the type safety.)
 
 
-## Logical Connectives as Inductive Types
+Logical Connectives as Inductive Types
+--------------------------------------
 
 > Inductive definitions are powerful enough to express most of the connectives we have seen so far. 
 > Indeed, only universal quantification (with implication as a special case) is built into Coq; 
@@ -284,7 +288,8 @@ Inductive or (P Q : Prop) : Prop :=
 this explains why `destruct` works but `split` not..
 
 
-## Q&A - Slide 22 + 24
+Q&A - Slide 22 + 24
+-------------------
 
 Both Question asked about what's the type of some expression
 
@@ -397,7 +402,8 @@ Inductive False : Prop := .
 ```
 
 
-## Equality
+Equality
+--------
 
 ```coq
 Inductive eq {X:Type} : X → X → Prop :=
@@ -417,8 +423,9 @@ Notation "x == y" := (eq x y)
 > The reason is that Coq treats as "the same" any two terms that are convertible according to a simple set of computation rules.
 
 nothing in the unification engine but we relies on the _reduction engine_.
-(how much is it willing to do?)
-> Mtf: just running them! (since Coq is total!)
+
+> Q: how much is it willing to do?  
+> Mtf: just run them! (since Coq is total!)
 
 ```coq
 Lemma four: 2 + 2 == 1 + 3.
@@ -430,7 +437,8 @@ Qed.
 The `reflexivity` tactic is essentially just shorthand for `apply eq_refl`.
 
 
-## Slide Q & A
+Slide Q & A
+-----------
 
 - (4) has to be applicable thing, i.e. lambda, or "property" in the notion! 
 
@@ -454,13 +462,13 @@ In general, the `inversion` tactic...
    3. (apply `constructor` theorem), match the conclusion of `C`, calculates a set of equalities (some extra restrictions)
    4. adds these equalities
    5. if there is contradiction, `discriminate`, solve subgoal.
-   
+
 
 ### Q
 
-> Q: Can we write `+` in a communitive way?
+> Q: Can we write `+` in a communitive way?  
 > A: I don't believe so.
-   
+
 
 [Ground truth](https://en.wikipedia.org/wiki/Ground_truth)
  - provided by direct observation (instead of inference)
@@ -468,7 +476,7 @@ In general, the `inversion` tactic...
 [Ground term](https://en.wikipedia.org/wiki/Ground_expression#Ground_terms) 
  - that does not contain any free variables.
 
-Groundness 
+Groundness
  - 根基性?
 
 > Weird `Axiomness` might break the soundness of generated code in OCaml...
diff --git a/_posts/read_sf_lf/2019-01-10-sf-lf-10-ind-principle.md b/_posts/read_sf_lf/2019-01-10-sf-lf-10-ind-principle.md
index 5ed4798a853..0ba98c34247 100644
--- a/_posts/read_sf_lf/2019-01-10-sf-lf-10-ind-principle.md
+++ b/_posts/read_sf_lf/2019-01-10-sf-lf-10-ind-principle.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」10 IndPrinciples"
+title: "「SF-LC」10 IndPrinciples"
 subtitle: "Logical Foundations - Induction Principles"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-11-sf-lf-11-rel.md b/_posts/read_sf_lf/2019-01-11-sf-lf-11-rel.md
index 2dac4863e25..c319e07cbb2 100644
--- a/_posts/read_sf_lf/2019-01-11-sf-lf-11-rel.md
+++ b/_posts/read_sf_lf/2019-01-11-sf-lf-11-rel.md
@@ -1,19 +1,18 @@
 ---
-title: "「逻辑基础」11 Rel"
+title: "「SF-LC」11 Rel"
 subtitle: "Logical Foundations - Properties of Relations"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
 
-> Hux: 注意我把很多 relation 相关的知识记在 `5. Tactics` 里的。
-> 为了避免每次都要 grep 我在这里写一下
+> relation 与injective/surjective/bijective function 等相关的知识在 `5. Tactics` 里，为了避免每次都要 `grep` 我在这里写一下。
 
 
 Relations
@@ -29,19 +28,23 @@ I have been long confused with _Unary Relations vs. Binary Relation on the Same
 I thought they were same...but turns out they are totally different!
 
 
-#### Unary/1-place relation is __Predicate__! 
+#### Unary/1-place relation is __Predicate__ or __Property__! 
 
 Either defined via set `X ⊆ P` or `x ∈ P`,
 or defined via function `P : X -> Bool` or `P : X -> {⊥, ⊤}`.
 (usually used in Math. Logic)
 
+Property = Indicator Fn = characteristic Fn = Boolean Predicate Fn = Predicate
+- <https://en.wikipedia.org/wiki/Property_(mathematics)>
+- <https://en.wikipedia.org/wiki/Indicator_function>
+
 
 #### [Binary Relation/2-place relation](https://en.wikipedia.org/wiki/Binary_relation) 
 
 Defined via two sets : `R ⊆ X × Y` or `x, y ∈ R` or `xRy`.  (where `x ∈ X, y ∈ Y`.)
 or via function `R: X × Y -> Bool`.
 
-#### [Homogeneous Relation 同类（的）关系](https://en.wikipedia.org/wiki/Binary_relation#Homogeneous_relation)
+##### [Homogeneous Relation 同类（的）关系](https://en.wikipedia.org/wiki/Binary_relation#Homogeneous_relation)
 
 Specifically! when `X = Y`, is called a _homogeneous relation_: 
 
diff --git a/_posts/read_sf_lf/2019-01-12-sf-lf-12-imp.md b/_posts/read_sf_lf/2019-01-12-sf-lf-12-imp.md
index fcbc8f291fd..94fae0aece9 100644
--- a/_posts/read_sf_lf/2019-01-12-sf-lf-12-imp.md
+++ b/_posts/read_sf_lf/2019-01-12-sf-lf-12-imp.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」12 Imp"
+title: "「SF-LC」12 Imp"
 subtitle: "Logical Foundations - Simple Imperative Programs"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-13-sf-lf-13-imp-parser.md b/_posts/read_sf_lf/2019-01-13-sf-lf-13-imp-parser.md
index 8989a5da315..2c70989edad 100644
--- a/_posts/read_sf_lf/2019-01-13-sf-lf-13-imp-parser.md
+++ b/_posts/read_sf_lf/2019-01-13-sf-lf-13-imp-parser.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」13 ImpParser"
+title: "「SF-LC」13 ImpParser"
 subtitle: "Logical Foundations - Lexing And Parsing In Coq"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-14-sf-lf-14-imp-ceval.md b/_posts/read_sf_lf/2019-01-14-sf-lf-14-imp-ceval.md
index 8f15d3fadf8..d370371096c 100644
--- a/_posts/read_sf_lf/2019-01-14-sf-lf-14-imp-ceval.md
+++ b/_posts/read_sf_lf/2019-01-14-sf-lf-14-imp-ceval.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」14 ImpCEvalFun"
+title: "「SF-LC」14 ImpCEvalFun"
 subtitle: "Logical Foundations - An Evaluation Function For Imp"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-15-sf-lf-15-extraction.md b/_posts/read_sf_lf/2019-01-15-sf-lf-15-extraction.md
index 18e134ee921..9e5d542d613 100644
--- a/_posts/read_sf_lf/2019-01-15-sf-lf-15-extraction.md
+++ b/_posts/read_sf_lf/2019-01-15-sf-lf-15-extraction.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」15 Extraction"
+title: "「SF-LC」15 Extraction"
 subtitle: "Logical Foundations - Extracting ML From Coq"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_lf/2019-01-16-sf-lf-16-auto.md b/_posts/read_sf_lf/2019-01-16-sf-lf-16-auto.md
index 046f2958d35..2c7463d06a2 100644
--- a/_posts/read_sf_lf/2019-01-16-sf-lf-16-auto.md
+++ b/_posts/read_sf_lf/2019-01-16-sf-lf-16-auto.md
@@ -1,13 +1,13 @@
 ---
-title: "「逻辑基础」16 Auto"
+title: "「SF-LC」16 Auto"
 subtitle: "Logical Foundations - More Automation"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 逻辑基础
+  - LF (逻辑基础)
+  - SF (软件基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-01-sf-plf-01-equiv.md b/_posts/read_sf_plf/2019-03-01-sf-plf-01-equiv.md
index 701330432c1..afd5fdcd389 100644
--- a/_posts/read_sf_plf/2019-03-01-sf-plf-01-equiv.md
+++ b/_posts/read_sf_plf/2019-03-01-sf-plf-01-equiv.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」1 Equiv"
+title: "「SF-PLF」1 Equiv"
 subtitle: "Programming Language Foundations - Program Equivalence (程序的等价关系)"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-02-sf-plf-02-hoare-1.md b/_posts/read_sf_plf/2019-03-02-sf-plf-02-hoare-1.md
index eae72fa3f50..e0f5cc9ff3d 100644
--- a/_posts/read_sf_plf/2019-03-02-sf-plf-02-hoare-1.md
+++ b/_posts/read_sf_plf/2019-03-02-sf-plf-02-hoare-1.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」2 Hoare"
+title: "「SF-PLF」2 Hoare"
 subtitle: "Programming Language Foundations - Hoare Logic, Part I "
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-03-sf-plf-03-hoare-2.md b/_posts/read_sf_plf/2019-03-03-sf-plf-03-hoare-2.md
index 14801e85eed..e49d7f7a4c4 100644
--- a/_posts/read_sf_plf/2019-03-03-sf-plf-03-hoare-2.md
+++ b/_posts/read_sf_plf/2019-03-03-sf-plf-03-hoare-2.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」3 Hoare2"
+title: "「SF-PLF」3 Hoare2"
 subtitle: "Programming Language Foundations - Hoare Logic, Part II"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-04-sf-plf-04-hoare-logic.md b/_posts/read_sf_plf/2019-03-04-sf-plf-04-hoare-logic.md
index 6769ebcb059..56c61bc575b 100644
--- a/_posts/read_sf_plf/2019-03-04-sf-plf-04-hoare-logic.md
+++ b/_posts/read_sf_plf/2019-03-04-sf-plf-04-hoare-logic.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」4 HoareAsLogic"
+title: "「SF-PLF」4 HoareAsLogic"
 subtitle: "Programming Language Foundations - Hoare Logic as a Logic"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-05-sf-plf-05-smallstep.md b/_posts/read_sf_plf/2019-03-05-sf-plf-05-smallstep.md
index fc85576d63f..fd2d4b25d40 100644
--- a/_posts/read_sf_plf/2019-03-05-sf-plf-05-smallstep.md
+++ b/_posts/read_sf_plf/2019-03-05-sf-plf-05-smallstep.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」5 Smallstep"
+title: "「SF-PLF」5 Smallstep"
 subtitle: "Programming Language Foundations - Small-Step Operational Semantics"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-06-sf-plf-06-types.md b/_posts/read_sf_plf/2019-03-06-sf-plf-06-types.md
index 78d809849cf..dcb695851b7 100644
--- a/_posts/read_sf_plf/2019-03-06-sf-plf-06-types.md
+++ b/_posts/read_sf_plf/2019-03-06-sf-plf-06-types.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」6 Types"
+title: "「SF-PLF」6 Types"
 subtitle: "Programming Language Foundations - Type Systems"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-07-sf-plf-07-STLC.md b/_posts/read_sf_plf/2019-03-07-sf-plf-07-STLC.md
index ce201299cac..873ddb691ea 100644
--- a/_posts/read_sf_plf/2019-03-07-sf-plf-07-STLC.md
+++ b/_posts/read_sf_plf/2019-03-07-sf-plf-07-STLC.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」7 Stlc"
+title: "「SF-PLF」7 Stlc"
 subtitle: "Programming Language Foundations - The Simply Typed Lambda-Calculus"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-08-sf-plf-08-STLC-prop.md b/_posts/read_sf_plf/2019-03-08-sf-plf-08-STLC-prop.md
index 756be622ea9..3dee81a8b50 100644
--- a/_posts/read_sf_plf/2019-03-08-sf-plf-08-STLC-prop.md
+++ b/_posts/read_sf_plf/2019-03-08-sf-plf-08-STLC-prop.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」8 StlcProp"
+title: "「SF-PLF」8 StlcProp"
 subtitle: "Programming Language Foundations - Properties of STLC"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-09-sf-plf-09-more-STLC.md b/_posts/read_sf_plf/2019-03-09-sf-plf-09-more-STLC.md
index c0348e3b429..27b9b5ed0b7 100644
--- a/_posts/read_sf_plf/2019-03-09-sf-plf-09-more-STLC.md
+++ b/_posts/read_sf_plf/2019-03-09-sf-plf-09-more-STLC.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」9 MoreStlc"
+title: "「SF-PLF」9 MoreStlc"
 subtitle: "Programming Language Foundations - More on The Simply Typed Lambda-Calculus"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-10-sf-plf-10-subtyping.md b/_posts/read_sf_plf/2019-03-10-sf-plf-10-subtyping.md
index 78627ac21ae..fb316107b2f 100644
--- a/_posts/read_sf_plf/2019-03-10-sf-plf-10-subtyping.md
+++ b/_posts/read_sf_plf/2019-03-10-sf-plf-10-subtyping.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」10 Sub"
+title: "「SF-PLF」10 Sub"
 subtitle: "Programming Language Foundations - Subtyping (子类型化)"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-11-sf-plf-11-typechecking.md b/_posts/read_sf_plf/2019-03-11-sf-plf-11-typechecking.md
index 705c281169b..fcc7c239a56 100644
--- a/_posts/read_sf_plf/2019-03-11-sf-plf-11-typechecking.md
+++ b/_posts/read_sf_plf/2019-03-11-sf-plf-11-typechecking.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」11. TypeChecking"
+title: "「SF-PLF」11. TypeChecking"
 subtitle: "Programming Language Foundations - A Typechecker for STLC"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-12-sf-plf-12-records.md b/_posts/read_sf_plf/2019-03-12-sf-plf-12-records.md
index dc19a692946..1e2a18d4fb8 100644
--- a/_posts/read_sf_plf/2019-03-12-sf-plf-12-records.md
+++ b/_posts/read_sf_plf/2019-03-12-sf-plf-12-records.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」12 Records"
+title: "「SF-PLF」12 Records"
 subtitle: "Programming Language Foundations - Adding Records To STLC"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-13-sf-plf-13-references.md b/_posts/read_sf_plf/2019-03-13-sf-plf-13-references.md
index cd7d1836d5e..b99b99a9e9a 100644
--- a/_posts/read_sf_plf/2019-03-13-sf-plf-13-references.md
+++ b/_posts/read_sf_plf/2019-03-13-sf-plf-13-references.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」13 References"
+title: "「SF-PLF」13 References"
 subtitle: "Programming Language Foundations - Typing Mutable References"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-14-sf-plf-14-record-sub.md b/_posts/read_sf_plf/2019-03-14-sf-plf-14-record-sub.md
index 562c1671d0b..a4f0e5a4e1f 100644
--- a/_posts/read_sf_plf/2019-03-14-sf-plf-14-record-sub.md
+++ b/_posts/read_sf_plf/2019-03-14-sf-plf-14-record-sub.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」14 RecordSub"
+title: "「SF-PLF」14 RecordSub"
 subtitle: "Programming Language Foundations - Subtyping with Records"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-15-sf-plf-15-norm-STLC.md b/_posts/read_sf_plf/2019-03-15-sf-plf-15-norm-STLC.md
index 7e3665a0bdb..d15e83b2cdb 100644
--- a/_posts/read_sf_plf/2019-03-15-sf-plf-15-norm-STLC.md
+++ b/_posts/read_sf_plf/2019-03-15-sf-plf-15-norm-STLC.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」15 Norm"
+title: "「SF-PLF」15 Norm"
 subtitle: "Programming Language Foundations - Normalization of STLC"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-16-sf-plf-16-lib-tactics.md b/_posts/read_sf_plf/2019-03-16-sf-plf-16-lib-tactics.md
index 7a57a7e7003..60b51ab2a71 100644
--- a/_posts/read_sf_plf/2019-03-16-sf-plf-16-lib-tactics.md
+++ b/_posts/read_sf_plf/2019-03-16-sf-plf-16-lib-tactics.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」16 LibTactics"
+title: "「SF-PLF」16 LibTactics"
 subtitle: "Programming Language Foundations - A Collection of Handy General-Purpose Tactics"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-17-sf-plf-17-use-tactics.md b/_posts/read_sf_plf/2019-03-17-sf-plf-17-use-tactics.md
index 504be068ef0..3c3beb34c58 100644
--- a/_posts/read_sf_plf/2019-03-17-sf-plf-17-use-tactics.md
+++ b/_posts/read_sf_plf/2019-03-17-sf-plf-17-use-tactics.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」17 UseTactics"
+title: "「SF-PLF」17 UseTactics"
 subtitle: "Programming Language Foundations - Tactic Library For Coq"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-18-sf-plf-18-use-auto.md b/_posts/read_sf_plf/2019-03-18-sf-plf-18-use-auto.md
index cf9317108e1..0287e48c61b 100644
--- a/_posts/read_sf_plf/2019-03-18-sf-plf-18-use-auto.md
+++ b/_posts/read_sf_plf/2019-03-18-sf-plf-18-use-auto.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」18 UseAuto"
+title: "「SF-PLF」18 UseAuto"
 subtitle: "Programming Language Foundations - Theory And Practice Of Automation In Coq Proofs"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_plf/2019-03-19-sf-plf-19-partial-eval.md b/_posts/read_sf_plf/2019-03-19-sf-plf-19-partial-eval.md
index d769305d9f8..47666eab0d2 100644
--- a/_posts/read_sf_plf/2019-03-19-sf-plf-19-partial-eval.md
+++ b/_posts/read_sf_plf/2019-03-19-sf-plf-19-partial-eval.md
@@ -1,13 +1,13 @@
 ---
-title: "「编程语言基础」19 PE"
+title: "「SF-PLF」19 PE"
 subtitle: "Programming Language Foundations - Partial Evaluation"
 layout: post
 author: "Hux"
 header-style: text
 hidden: true
 tags:
-  - 软件基础
-  - 编程语言基础
+  - SF (软件基础)
+  - PLF (编程语言基础)
   - Coq
   - 笔记
 ---
diff --git a/_posts/read_sf_qc/2019-09-02-sf-qc-02-typeclasses.md b/_posts/read_sf_qc/2019-09-02-sf-qc-02-typeclasses.md
new file mode 100644
index 00000000000..79acd51316d
--- /dev/null
+++ b/_posts/read_sf_qc/2019-09-02-sf-qc-02-typeclasses.md
@@ -0,0 +1,796 @@
+---
+title: "「SF-QC」2 TypeClasses"
+subtitle: "Quickcheck - A Tutorial on Typeclasses in Coq"
+layout: post
+author: "Hux"
+header-style: text
+hidden: true
+tags:
+  - SF (软件基础)
+  - QC (Quickcheck)
+  - Coq
+  - 笔记
+---
+
+Considerring printing different types with this common idiom:
+
+```coq
+showBool : bool → string
+showNat : nat → string
+showList : {A : Type} (A → string) → (list A) → string
+showPair : {A B : Type} (A → string) → (B → string) → A * B → string
+
+Definition showListOfPairsOfNats := showList (showPair showNat showNat)   (* LOL *)
+```
+
+> The designers of Haskell addressed this clunkiness through _typeclasses_, a mechanism by which the typechecker is instructed to automatically construct "type-driven" functions [Wadler and Blott 1989].
+
+Coq followed Haskell's lead as well, but
+
+> because Coq's type system is so much richer than that of Haskell, and because typeclasses in Coq are used to automatically construct not only programs but also proofs, Coq's presentation of typeclasses is quite a bit less "transparent"
+
+
+Basics
+------
+
+### Classes and Instances
+
+```coq
+Class Show A : Type := {
+  show : A → string
+}.
+
+Instance showBool : Show bool := {
+  show := fun b:bool ⇒ if b then "true" else "false"
+}.
+```
+
+Comparing with Haskell:
+
+```haskell
+class Show a where
+  show :: a -> string
+
+--  you cannot override a `instance` so in reality you need a `newtype` wrapper to do this
+instance Show Bool where
+  show b = if b then "True" else "Fasle"
+```
+
+> The show function is sometimes said to be overloaded, since it can be applied to arguments of many types, with potentially radically different behavior depending on the type of its argument.
+
+
+Next, we can define functions that use the overloaded function show like this:
+
+```coq
+Definition showOne {A : Type} `{Show A} (a : A) : string :=
+  "The value is " ++ show a.
+  
+Compute (showOne true).
+Compute (showOne 42).
+
+Definition showTwo {A B : Type}
+           `{Show A} `{Show B} (a : A) (b : B) : string :=
+  "First is " ++ show a ++ " and second is " ++ show b.
+
+Compute (showTwo true 42).
+Compute (showTwo Red Green).
+```
+
+> The parameter `` `{Show A}`` is a _class constraint_, which states that the function showOne is expected to be applied only to types A that belong to the Show class.
+
+> Concretely, this constraint should be thought of as an _extra parameter_ to showOne supplying _evidence_ that A is an instance of Show — i.e., it is essentially just a show function for A, which is implicitly invoked by the expression show a.
+
+读时猜测（后来发现接下来有更正确的解释）：`show` 在 name resolution 到 `class Show` 时就可以根据其参数的 type（比如 `T`）infer 出「我们需要一个 `Show T` 的实现（`instance`，其实就是个 table）」，在 Haskell/Rust 中这个 table 会在 lower 到 IR 时才 made explicit，而 Coq 这里的语法就已经强调了这里需要 implicitly-and-inferred `{}` 一个 table，这个 table 的名字其实不重要，只要其 type 是被 `A` parametrized 的 `Show` 就好了，类似 ML 的 `functor` 或者 Java 的 generic `interface`。
+
+This is _Ad-hoc polymorphism_.
+
+
+#### Missing Constraint
+
+What if we forget the class constrints:
+
+```coq
+Error:
+Unable to satisfy the following constraints:
+In environment:
+A : Type
+a : A
+
+?Show : "Show A"
+```
+
+
+#### Class `Eq`
+
+```coq
+Class Eq A :=
+  {
+    eqb: A → A → bool;
+  }.
+
+Notation "x =? y" := (eqb x y) (at level 70).
+
+Instance eqBool : Eq bool :=
+  {
+    eqb := fun (b c : bool) ⇒ 
+       match b, c with
+         | true, true ⇒ true
+         | true, false ⇒ false
+         | false, true ⇒ false
+         | false, false ⇒ true
+       end
+  }.
+
+Instance eqNat : Eq nat :=
+  {
+    eqb := Nat.eqb
+  }.
+```
+
+> Why should we need to define a typeclass for boolean equality when _Coq's propositional equality_ (`x = y`) is completely generic? 
+> while it makes sense to _claim_ that two values `x` and `y` are equal no matter what their type is, it is not possible to write a _decidable equality checker_ for arbitrary types. In particular, equality at types like `nat → nat` is undecidable.
+
+`x = y` 返回一个需要去证的 `Prop` (relational) 而非 executable `Fixpoint` (functional)  
+因为 function 的 equality 有时候会 undeciable，所以才需要加 Functional Extensionality `Axiom`（见 LF-06）
+
+```coq
+Instance eqBoolArrowBool: Eq (bool -> bool) :=
+  {
+    eqb := fun (f1 f2 : bool -> bool) =>
+      (f1 true) =? (f2 true) && (f1 false) =? (f2 false) 
+  }.
+
+Compute (id =? id).      (* ==> true *)
+Compute (negb =? negb).  (* ==> true *)
+Compute (id =? negb).    (* ==> false *)
+```
+
+这里这个 `eqb` 的定义也是基于 extensionality 的定义，如果考虑到 effects（divergence、IO）是很容易 break 的（类似 parametricity）
+
+
+
+### Parameterized Instances: New Typeclasses from Old
+
+Structural recursion 
+
+```coq
+Instance showPair {A B : Type} `{Show A} `{Show B} : Show (A * B) :=
+  {
+    show p :=
+      let (a,b) := p in 
+        "(" ++ show a ++ "," ++ show b ++ ")"
+  }.
+Compute (show (true,42)).
+```
+
+Structural equality
+
+```coq
+Instance eqPair {A B : Type} `{Eq A} `{Eq B} : Eq (A * B) :=
+  {
+    eqb p1 p2 :=
+      let (p1a,p1b) := p1 in
+      let (p2a,p2b) := p2 in
+      andb (p1a =? p2a) (p1b =? p2b)
+  }.
+```
+
+Slightly more complicated example: typical list:
+
+```coq
+(* the book didn't use any from ListNotation *)
+Fixpoint showListAux {A : Type} (s : A → string) (l : list A) : string :=
+  match l with
+    | nil ⇒ ""
+    | cons h nil ⇒ s h
+    | cons h t ⇒ append (append (s h) ", ") (showListAux s t)
+  end.
+Instance showList {A : Type} `{Show A} : Show (list A) :=
+  {
+    show l := append "[" (append (showListAux show l) "]")
+  }.
+  
+(* I used them though *)
+Fixpoint eqListAux {A : Type} `{Eq A} (l1 l2 : list A) : bool :=
+  match l1, l2 with
+    | nil, nil => true
+    | (h1::t1), (h2::t2) => (h1 =? h2) && (eqListAux t1 t2)
+    | _, _ => false
+  end.
+
+Instance eqList {A : Type} `{Eq A} : Eq (list A) :=
+  {
+    eqb l1 l2 := eqListAux l1 l2
+  }.
+```
+
+
+
+### Class Hierarchies
+
+> we might want a typeclass `Ord` for "ordered types" that support both equality and a less-or-equal comparison operator.
+
+A bad way would be declare a new class with two func `eq` and `le`.
+
+It's better to establish dependencies between typeclasses, similar with OOP `class` inheritence and subtyping (but better!), this gave good code reuses.
+
+> We often want to organize typeclasses into hierarchies.
+
+```coq
+Class Ord A `{Eq A} : Type :=
+  {
+    le : A → A → bool
+  }.
+Check Ord. (* ==>
+Ord
+     : forall A : Type, Eq A -> Type
+*)
+```
+
+class `Eq` is a "super(type)class" of `Ord` (not to be confused with OOP superclass)
+
+This is _Sub-typeclassing_.
+
+```coq
+Fixpoint listOrdAux {A : Type} `{Ord A} (l1 l2 : list A) : bool := 
+  match l1, l2 with
+  | [], _ => true
+  | _, [] => false
+  | h1::t1, h2::t2 => if (h1 =? h2)
+                     then (listOrdAux t1 t2)
+                     else (le h1 h2)
+  end.
+
+Instance listOrd {A : Type} `{Ord A} : Ord (list A) :=
+  {
+    le l1 l2 := listOrdAux l1 l2
+  }.
+
+(* truthy *)
+Compute (le [1] [2]).
+Compute (le [1;2] [2;2]).
+Compute (le [1;2;3] [2]).
+
+(* falsy *)
+Compute (le [1;2;3] [1]).
+Compute (le [2] [1;2;3]).
+```
+
+
+
+How It works
+------------
+
+### Implicit Generalization
+
+所以 `` `{...}`` 这个 "backtick" notation is called _implicit generalization_，比 implicit `{}` 多做了一件自动 generalize 泛化 free varabile 的事情。
+
+> that was added to Coq to support typeclasses but that can also be used to good effect elsewhere.
+
+```coq
+Definition showOne1 `{Show A} (a : A) : string :=
+  "The value is " ++ show a.
+
+Print showOne1.
+(* ==>
+    showOne1 = 
+      fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a
+           : forall A : Type, Show A -> A -> string
+
+    Arguments A, H are implicit and maximally inserted
+*)
+```
+
+> notice that the occurrence of `A` inside the `` `{...}`` is unbound and automatically insert the binding that we wrote explicitly before.
+
+> The "implicit and maximally generalized" annotation on the last line means that the automatically inserted bindings are treated (注：printed) as if they had been written with `{...}`, rather than `(...)`.
+
+> The "implicit" part means that the type argument `A` and the `Show` witness `H` are usually expected to be left implicit  
+> whenever we write `showOne1`, Coq will automatically insert two _unification variables_ as the first two arguments.
+
+> This automatic insertion can be disabled by writing `@`, so a bare occurrence of `showOne1` means the same as `@showOne1 _ _`
+
+这里的 witness `H` 即 `A` implements `Show` 的 evidence，本质就是个 table or record，可以 written more explicitly:
+
+```coq
+Definition showOne2 `{_ : Show A} (a : A) : string :=
+  "The value is " ++ show a.
+
+Definition showOne3 `{H : Show A} (a : A) : string :=
+  "The value is " ++ show a.
+```
+
+甚至 
+
+```coq
+Definition showOne4 `{Show} a : string :=
+  "The value is " ++ show a.
+```
+
+```coq
+showOne = 
+fun (A : Type) (H : Show A) (a : A) => "The value is " ++ show a
+     : forall A : Type, Show A -> A -> string
+
+Set Printing Implicit.
+
+showOne = 
+fun (A : Type) (H : Show A) (a : A) => "The value is " ++ @show A H a     (* <-- 注意这里 *)
+     : forall A : Type, Show A -> A -> string
+```
+
+#### vs. Haskell
+
+顺便，Haskell 的话，`Show` 是可以直接 inferred from the use of `show` 得
+
+```haskell
+Prelude> showOne a = show a
+Prelude> :t showOne
+showOne :: Show a => a -> String
+```
+
+但是 Coq 不行，会退化上「上一个定义的 instance Show」，还挺奇怪的（
+
+```coq
+Definition showOne5 a : string :=  (* not generalized *)
+  "The value is " ++ show a.
+```
+
+#### Free Superclass Instance
+
+``{Ord A}` led Coq to fill in both `A` and `H : Eq A` because it's the superclass of `Ord` (appears as the second argument). 
+
+```coq
+Definition max1 `{Ord A} (x y : A) :=
+  if le x y then y else x.
+
+Set Printing Implicit.
+Print max1.
+(* ==>
+     max1 = 
+       fun (A : Type) (H : Eq A) (H0 : @Ord A H) (x y : A) =>
+         if @le A H H0 x y then y else x
+
+   : forall (A : Type) (H : Eq A), 
+       @Ord A H -> A -> A -> A    
+*)
+Check Ord.
+(* ==> Ord : forall A : Type, Eq A -> Type *)
+```
+
+`Ord` type 写详细的话可以是：
+
+```coq
+Ord : forall (A : Type), (H: Eq A) -> Type
+```
+
+
+#### Other usages of `` `{} ``
+
+Implicit generalized `Prop` mentioning free vars.
+
+```coq
+Generalizable Variables x y.
+
+Lemma commutativity_property : `{x + y = y + x}.
+Proof. intros. omega. Qed.
+
+Check commutativity_property.
+```
+
+Implicit generalized `fun`/`λ`, however...
+
+```coq
+Definition implicit_fun := `{x + y}.
+Compute (implicit_fun 2 3)  (* ==> Error *)
+Compute (@implicit_fun 2 3)
+```
+
+Implicitly-generalized but inserted as explicit via `` `(...)``
+
+```coq
+Definition implicit_fun := `(x + y).
+Compute (implicit_fun 2 3)
+```
+
+这里可以看到 Coq 的所有语法都是正交的（非常牛逼……）
+- `()`/`{}` 控制是否是 implicit argument
+- `` ` ``-prefix 控制是否做 implicit generalization
+  - N.B. 可能你忘记了但是 `→` is degenerated `∀` (`Π`)，所以 generalization 自然会生成 `fun`
+
+
+### Records are Products
+
+> Record types must be declared before they are used. For example:
+
+```coq
+Record Point :=
+  Build_Point
+    {
+      px : nat;
+      py : nat
+    }.
+
+(* built with constructor *)
+Check (Build_Point 2 4).
+
+(* built with record syntax *)
+Check {| px := 2; py := 4 |}.
+Check {| py := 2; px := 4 |}.
+
+(* field access, with a clunky "dot notation" *)
+Definition r : Point := {| px := 2; py := 4 |}.
+Compute (r.(px) + r.(py)).
+```
+
+和 OCaml 一样是 nominal typing 而非 structural typing。
+类似于 OCaml 中的 record 其实到 backend 了就会和 tuple 等价：都会 lower 到 Heap Block），
+Coq 中的 Record 其实和 Pair/Product 也是等价：都是 arity 为 2 的 Inductive type：
+
+```coq
+Inductive Point : Set := 
+  | Build_Point : nat → nat → Point.
+```
+
+我仿造 `Print px.` 输出的定义模拟了一下：
+
+```coq
+Inductive Point2 : Set := 
+  | Build_Point2 (px2:nat) (py2:nat).
+Definition px2 := fun p : Point2 => let (px, _) := p in px.
+Definition py2 := fun p : Point2 => let (_, py) := p in py.
+
+Definition r2 : Point2 := Build_Point2 2 4.
+Compute (r2.(px2) + r2.(py2)).                        (* => 6 *)
+
+Definition r2 : Point2 := {| px2 := 2; py2 := 4 |}.   (* Error: px2 is not a projection *)
+```
+
+可以发现 dot notation 是可以工作的，`.` 应该只是一个 pipe
+但是 `{|...|}` 不知道为什么这里会认为 `px2` 不是一个 record projection.
+
+
+> Note that the field names have to be different. Any given field name can belong to only one record type. 
+> This greatly simplifies type inference!
+
+
+### Typeclasses are Records
+
+> Typeclasses and instances, in turn, are basically just syntactic sugar for record types and values (together with a bit of magic for using proof search to fill in appropriate instances during typechecking...
+
+> Internally, a typeclass declaration is elaborated into a _parameterized_ `Record` declaration:
+
+```coq
+Class Show A : Type := { show : A → string }.
+
+Print Show.
+Record Show (A : Type) : Type := 
+    Build_Show { show : A -> string }
+
+Set Printing All.
+Print Show.
+Variant Show (A : Type) : Type :=
+    Build_Show : forall _ : forall _ : A, string, Show A
+
+(* to make it more clear... *)
+Inductive Show (A : Type) : Type :=
+  | Build_Show : ∀(show : ∀(a : A), string), Show A
+  
+(* or more GADT looking, i.e., implicit generalized *)
+Inductive Show (A : Type) : Type :=
+  | Build_Show : (A -> string) -> Show A
+```
+
+Coq actually call a single-field record `Variant`. 
+Well actually, I found it's for any single-constructor `Inductive`ly constructed type. 
+You can even use `Variant` nonchangbly with `Inductive` as a keyword...
+
+```coq
+Set Printing All.
+Print Point.
+Variant Point : Set :=
+    Build_Point : forall (_ : nat) (_ : nat), Point
+```
+
+> Analogously, Instance declarations become record values:
+
+```coq
+Print showNat.
+showNat = {| show := string_of_nat |}
+    : Show nat
+```
+
+> Similarly, overloaded functions like show are really just _record projections_, which in turn are just functions that select a particular argument of a one-constructor Inductive type.
+
+```coq
+Print show.
+show = 
+  fun (A : Type) (Show0 : Show A) => 
+    let (show) := Show0 in show
+      : forall A : Type, Show A -> A -> string
+
+Set Printing All.
+Print show.
+show = 
+  fun (A : Type) (Show0 : Show A) =>
+    match Show0 return (forall _ : A, string) with
+    | Build_Show _ show => show
+    end
+      : forall (A : Type) (_ : Show A) (_ : A), string
+```
+
+
+### Inferring Instances
+
+> appropriate instances are automatically inferred (and/or constructed!) during typechecking.
+
+```coq
+Definition eg42 := show 42.
+
+Set Printing Implicit.
+Print eg42.
+eg42 = @show nat showNat 42 : string
+```
+
+different with `Compute`, `Print` 居然还可以这么把所有 implicit argument (after inferred) 都给 print 出来……
+
+type inferrence: 
+
+- `show` is expanded to `@show _ _ 42`
+- obviously it's `@show nat __42`
+- obviously it's `@show nat (?H : Show Nat) 42`
+
+Okay now where to find this witness/evidence/instance/record/table/you-name-it `?H` 
+
+> It attempts to find or construct such a value using a _variant of the `eauto` proof search_ procedure that refers to a "hint database" called `typeclass_instances`.
+
+```coq
+Print HintDb typeclass_instances.  (* too much to be useful *)
+```
+
+"hint database" to me is better understood as a reverse of environment or typing context `Γ`. Though specialized with only `Instance` there.
+（这么一看实现一个 Scala 的 `Implicit` 也不难啊）
+
+Coq can even print what's happening during this proof search!
+
+```coq
+Set Typeclasses Debug.
+Check (show 42).
+(* ==>
+     Debug: 1: looking for (Show nat) without backtracking
+     Debug: 1.1: exact showNat on (Show nat), 0 subgoal(s)
+*)
+
+Check (show (true,42)).
+(* ==>
+     Debug: 1: looking for (Show (bool * nat)) without backtracking
+     Debug: 1.1: simple apply @showPair on (Show (bool * nat)), 2 subgoal(s)
+     Debug: 1.1.3 : (Show bool)
+     Debug: 1.1.3: looking for (Show bool) without backtracking
+     Debug: 1.1.3.1: exact showBool on (Show bool), 0 subgoal(s)
+     Debug: 1.1.3 : (Show nat)
+     Debug: 1.1.3: looking for (Show nat) without backtracking
+     Debug: 1.1.3.1: exact showNat on (Show nat), 0 subgoal(s)      *)
+Unset Typeclasses Debug.
+```
+
+> In summary, here are the steps again:
+
+```coq
+show 42
+    ===>   { Implicit arguments }
+@show _ _ 42
+    ===>   { Typing }
+@show (?A : Type) (?Show0 : Show ?A) 42
+    ===>   { Unification }
+@show nat (?Show0 : Show nat) 42
+    ===>   { Proof search for Show Nat returns showNat }
+@show nat showNat 42
+```
+
+
+Typeclasses and Proofs
+----------------------
+
+### Propositional Typeclass Members
+
+```coq
+Class EqDec (A : Type) {H : Eq A} := 
+  { 
+    eqb_eq : ∀ x y, x =? y = true ↔ x = y 
+  }.
+```
+
+```coq
+Instance eqdecNat : EqDec nat := 
+  {
+    eqb_eq := Nat.eqb_eq
+  }.
+```
+
+这里可以用于抽象 LF-07 的 reflection
+
+
+### Substructures
+
+> Naturally, it is also possible to have typeclass instances as members of other typeclasses: these are called _substructures_. 
+
+这里的 `relation` 来自 Prelude 不过和 LF-11 用法一样：
+
+```coq
+Require Import Coq.Relations.Relation_Definitions.
+Class Reflexive (A : Type) (R : relation A) :=
+  { 
+    reflexivity : ∀ x, R x x
+  }.
+Class Transitive (A : Type) (R : relation A) :=
+  {
+    transitivity : ∀ x y z, R x y → R y z → R x z
+  }.
+```
+
+```coq
+Class PreOrder (A : Type) (R : relation A) :=
+  { PreOrder_Reflexive :> Reflexive A R ;
+    PreOrder_Transitive :> Transitive A R }.
+```
+
+> The syntax `:>` indicates that each `PreOrder` can be seen as a `Reflexive` and `Transitive` relation, so that, any time a reflexive relation is needed, a preorder can be used instead.
+
+这里的 `:>` 方向和 subtyping 的 _subsumption_ 是反着的……跟 SML 的 ascription `:>` 一样……
+
+- subtyping  `T :> S` : value of `S` can safely be used as value of `T`
+- ascription `P :> R` : value of `P` can safely be used as value of `R`
+
+Why?
+
+
+
+Some Useful Typeclasses
+-----------------------
+
+### `Dec`
+
+> The `ssreflect` library defines what it means for a proposition `P` to be _decidable_ like this...
+
+```coq
+Require Import ssreflect ssrbool.
+Print decidable.
+(* ==>
+     decidable = fun P : Prop => {P} + {~ P}
+*)
+```
+
+> .. where `{P} + {¬ P}` is an "informative disjunction" of `P` and `¬P`.
+
+即两个 evidence（参考 LF-07)
+
+```coq
+Class Dec (P : Prop) : Type :=
+  {
+    dec : decidable P
+  }.
+```
+
+### Monad
+
+> In Haskell, one place typeclasses are used very heavily is with the Monad typeclass, especially in conjunction with Haskell's "do notation" for monadic actions.
+
+> Monads are an extremely powerful tool for organizing and streamlining code in a wide range of situations where computations can be thought of as yielding a result along with some kind of "effect."
+
+说话很严谨「in a wide range of situations where ... "effect"」
+
+> most older projects simply define their own monads and monadic notations — sometimes typeclass-based, often not — while newer projects use one of several generic libraries for monads. Our current favorite (as of Summer 2017) is the monad typeclasses in Gregory Malecha's `ext-lib` package:
+
+<https://github.com/coq-ext-lib/coq-ext-lib/blob/v8.5/theories/Structures/Monad.v>
+
+```coq
+Require Export ExtLib.Structures.Monads.
+Export MonadNotation.
+Open Scope monad_scope.
+```
+
+```coq
+Class Monad (M : Type → Type) : Type := { 
+  ret : ∀ {T : Type}, T → M T ;
+  bind : ∀ {T U : Type}, M T → (T → M U) → M U
+}.
+
+Instance optionMonad : Monad option := {
+  ret T x := Some x ;
+  bind T U m f :=
+    match m with
+      None ⇒ None
+    | Some x ⇒ f x
+    end
+}.
+```
+
+Compare with Haskell:
+
+```haskell
+class Applicative m => Monad (m :: * -> *) where
+  return :: a -> m a
+  (>>=) :: m a -> (a -> m b) -> m b
+  
+instance Monad Maybe where
+  return = Just
+  (>>=)  = (>>=)
+  where
+    (>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
+    Nothing  >>= _ = Nothing
+    (Just x) >>= f = f x
+```
+
+After mimic `do` notation: (as PLF-11)
+
+```coq
+Definition sum3 (l : list nat) : option nat :=
+  x0 <- nth_opt 0 l ;;
+  x1 <- nth_opt 1 l ;;
+  x2 <- nth_opt 2 l ;;
+  ret (x0 + x1 + x2).
+```
+
+
+Controlling Instantiation
+-------------------------
+
+### "Defaulting"
+
+Would better explicitly typed. searching can be stupid
+
+### Manipulating the Hint Database
+
+> One of the ways in which Coq's typeclasses differ most from Haskell's is the lack, in Coq, of an automatic check for "overlapping instances."
+
+在 Haskell 中一大 use case 是可以做类似 C++ 的 partial specification（偏特化）
+
+- Check out [this](https://kseo.github.io/posts/2017-02-05-avoid-overlapping-instances-with-closed-type-families.html) on the pros and cons of overlapping instances in Haskell
+- Check out [this] (https://www.ibm.com/developerworks/community/blogs/12bb75c9-dfec-42f5-8b55-b669cc56ad76/entry/c__e6_a8_a1_e6_9d_bf__e7_a9_b6_e7_ab_9f_e4_bb_80_e4_b9_88_e6_98_af_e7_89_b9_e5_8c_96?lang=en) on template partial specification in C++
+
+> That is, it is completely legal to define a given type to be an instance of a given class in two different ways.
+> When this happens, it is unpredictable which instance will be found first by the instance search process;
+
+Workarounds in Coq when this happen:
+1. removing instances from hint database
+2. priorities
+
+
+
+Debugging
+---------
+
+TBD.
+
+- Instantiation Failures
+- Nontermination
+
+
+Alternative Structuring Mechanisms
+----------------------------------
+
+_large-scale structuring mechanisms_
+
+> Typeclasses are just one of several mechanisms that can be used in Coq for structuring large developments. Others include:
+>
+> - canonical structures
+> - bare dependent records
+> - modules and functors
+
+Module and functors is very familiar!
+
+
+Further Reading
+----------------------------------
+
+On the origins of typeclasses in Haskell:
+
+- How to make ad-hoc polymorphism less ad hoc Philip Wadler and Stephen Blott. 16'th Symposium on Principles of Programming Languages, ACM Press, Austin, Texas, January 1989.
+  <http://homepages.inf.ed.ac.uk/wadler/topics/type-classes.html>  
+
+The original paper on typeclasses In Coq:
+
+- Matthieu Sozeau and Nicolas Oury. First-Class Type Classes. TPHOLs 2008.
+  <https://link.springer.com/chapter/10.1007%2F978-3-540-71067-7_23>
+  
diff --git a/css/hux-blog.css b/css/hux-blog.css
index 8ebaddecc11..4daec2898eb 100644
--- a/css/hux-blog.css
+++ b/css/hux-blog.css
@@ -718,7 +718,7 @@ samp {
   margin-bottom: 30px;
 }
 .post-container h4 {
-  font-size: 19px;
+  font-size: 22px;
   font-weight: 600;
   color: gray;
 }
@@ -727,7 +727,7 @@ samp {
 }
 .post-container h5,
 .post-container h6 {
-  font-size: 17px;
+  font-size: 20px;
   font-weight: 600;
   color: gray;
 }
@@ -743,9 +743,13 @@ samp {
     font-size: 22px;
   }
   .post-container h3 {
-    font-size: 19px;
+    font-size: 20px;
   }
   .post-container h4 {
+    font-size: 19px;
+  }
+  .post-container h5,
+  .post-container h6 {
     font-size: 18px;
   }
 }
diff --git a/css/hux-blog.min.css b/css/hux-blog.min.css
index 3037759ff45..0ed7f1d94c3 100644
--- a/css/hux-blog.min.css
+++ b/css/hux-blog.min.css
@@ -1 +1 @@
-@media (min-width:1200px){.post-container,.sidebar-container{padding-right:5%}}@media (min-width:768px){.post-container{padding-right:5%}}.sidebar-container{color:#bfbfbf;font-size:14px}.sidebar-container h5{color:#ccc;padding-bottom:1em}.sidebar-container h5 a{color:#ccc!important;text-decoration:none}.sidebar-container a{color:#bfbfbf!important}.sidebar-container a:hover,.sidebar-container a:active{color:#0085a1!important}.sidebar-container .tags a{border-color:#bfbfbf}.sidebar-container .tags a:hover,.sidebar-container .tags a:active{border-color:#0085a1}.sidebar-container .short-about img{width:80%;display:block;border-radius:5px;margin-bottom:20px}.sidebar-container .short-about p{margin-top:0;margin-bottom:20px}.sidebar-container .short-about .list-inline>li{padding-left:0}.catalog-container{padding:0}.side-catalog{display:block;overflow:auto;height:100%;padding-bottom:40px;width:195px}.side-catalog.fixed{position:fixed;top:-21px}.side-catalog.fold .catalog-toggle::before{content:"+"}.side-catalog.fold .catalog-body{display:none}.side-catalog .catalog-toggle::before{content:"−";position:relative;margin-right:5px;bottom:1px}.side-catalog .catalog-body{position:relative;list-style:none;height:auto;overflow:hidden;padding-left:0;padding-right:5px;text-indent:0}.side-catalog .catalog-body li{position:relative;list-style:none}.side-catalog .catalog-body li a{padding-left:10px;max-width:180px;display:inline-block;vertical-align:middle;height:30px;line-height:30px;overflow:hidden;text-decoration:none;white-space:nowrap;text-overflow:ellipsis}.side-catalog .catalog-body .h1_nav,.side-catalog .catalog-body .h2_nav,.side-catalog .catalog-body .h3_nav{margin-left:0;font-size:13px;font-weight:700}.side-catalog .catalog-body .h4_nav,.side-catalog .catalog-body .h5_nav,.side-catalog .catalog-body .h6_nav{margin-left:10px;font-size:12px}.side-catalog .catalog-body .h4_nav a,.side-catalog .catalog-body .h5_nav a,.side-catalog .catalog-body .h6_nav a{max-width:170px}.side-catalog .catalog-body .active{border-radius:4px;background-color:#F5F5F5}.side-catalog .catalog-body .active a{color:#0085a1!important}@media (max-width:1200px){.side-catalog{display:none}}.paper-snackbar{transition-property:opacity,bottom,left,right,width,margin,border-radius;transition-duration:.5s;transition-timing-function:ease;font-size:14px;min-height:14px;background-color:#323232;background-color:#0085a1;position:fixed;display:flex;justify-content:space-between;align-items:center;color:#fff;line-height:22px;padding:18px 24px;bottom:0;opacity:0}@media (min-width:640px){.paper-snackbar{min-width:288px;max-width:568px;display:inline-flex;border-radius:2px;margin:24px;bottom:-100px}}@media (max-width:640px){.paper-snackbar{left:0;right:0}}.paper-snackbar .action{background:inherit;display:inline-block;border:none;font-size:inherit;text-transform:uppercase;color:#ffeb3b;margin:0 0 0 24px;padding:0;min-width:min-content;outline:0}.paper-button{position:relative;padding:4px 0;margin:1em;width:160px;overflow:hidden;user-select:none;color:#000;text-transform:uppercase;border-radius:3px;outline-color:#ccc}.paper-button:hover{cursor:pointer}.paper-button button,.paper-button input[type=submit]{background:inherit;border:none;display:block;width:100%;height:100%;font-size:1em;color:#000;text-transform:uppercase}.paper-button.colored,.paper-button.colored button{color:#4285f4}.paper-button.raised-button.colored{background-color:#4285f4}.paper-button .raised-button{box-shadow:0 2px 5px 0 rgba(0,0,0,.26)}.paper-button.raised-button.colored{background:#4285f4;color:#fff}.paper-button[disabled]{background-color:#EAEAEA!important;color:#A8A8A8!important;cursor:auto}.paper-button:hover{background-color:#EAEAEA}.paper-button.raised-button.colored:hover{background-color:#3367d6}button.paper-button{border:0;font-size:1em;line-height:25px;background-color:#fff}.paper-button input[type=submit]{outline-color:#ccc}.paper-button.colored.raised-button input[type=submit]{color:#fff}.paper-shadow-animated.paper-shadow{transition:box-shadow .28s cubic-bezier(0.4,0,.2,1)}.paper-shadow-top-z-1{box-shadow:0 2px 10px 0 rgba(0,0,0,.16)}.paper-shadow-bottom-z-1{box-shadow:0 2px 5px 0 rgba(0,0,0,.26)}.paper-shadow-top-z-2{box-shadow:0 6px 20px 0 rgba(0,0,0,.19)}.paper-shadow-bottom-z-2{box-shadow:0 8px 17px 0 rgba(0,0,0,.2)}.paper-shadow-top-z-3{box-shadow:0 17px 50px 0 rgba(0,0,0,.19)}.paper-shadow-bottom-z-3{box-shadow:0 12px 15px 0 rgba(0,0,0,.24)}.paper-shadow-top-z-4{box-shadow:0 25px 55px 0 rgba(0,0,0,.21)}.card{background:#fff;width:300px;height:300px;position:relative;margin:16px;border-radius:2px}.highlight,pre.highlight{background:#282c34;color:#abb2bf}.highlight pre{background:#282c34}.highlight .hll{background:#282c34}.highlight .c{color:#5c6370;font-style:italic}.highlight .err{color:#960050;background-color:#1e0010}.language-coq .highlight .err{background-color:transparent}.highlight .k,.language-coq .highlight .err{color:#c678dd}.highlight .l{color:#98c379}.highlight .n{color:#abb2bf}.highlight .o{color:#abb2bf}.highlight .p{color:#abb2bf}.highlight .cm{color:#5c6370;font-style:italic}.highlight .cp{color:#5c6370;font-style:italic}.highlight .c1{color:#5c6370;font-style:italic}.highlight .cs{color:#5c6370;font-style:italic}.highlight .ge{font-style:italic}.highlight .gs{font-weight:700}.highlight .kc{color:#c678dd}.highlight .kd{color:#c678dd}.highlight .kn{color:#c678dd}.highlight .kp{color:#c678dd}.highlight .kr{color:#c678dd}.highlight .kt{color:#c678dd}.highlight .ld{color:#98c379}.highlight .m{color:#d19a66}.highlight .s{color:#98c379}.highlight .na{color:#d19a66}.highlight .nb{color:#e5c07b}.highlight .nc{color:#e5c07b}.highlight .no{color:#e5c07b}.highlight .nd{color:#e5c07b}.highlight .ni{color:#e5c07b}.highlight .ne{color:#e5c07b}.highlight .nf{color:#abb2bf}.highlight .nl{color:#e5c07b}.highlight .nn{color:#abb2bf}.highlight .nx{color:#abb2bf}.highlight .py{color:#e5c07b}.highlight .nt{color:#e06c75}.highlight .nv{color:#e5c07b}.highlight .ow{font-weight:700}.highlight .w{color:#f8f8f2}.highlight .mf{color:#d19a66}.highlight .mh{color:#d19a66}.highlight .mi{color:#d19a66}.highlight .mo{color:#d19a66}.highlight .sb{color:#98c379}.highlight .sc{color:#98c379}.highlight .sd{color:#98c379}.highlight .s2{color:#98c379}.highlight .se{color:#98c379}.highlight .sh{color:#98c379}.highlight .si{color:#98c379}.highlight .sx{color:#98c379}.highlight .sr{color:#56b6c2}.highlight .s1{color:#98c379}.highlight .ss{color:#56b6c2}.highlight .bp{color:#e5c07b}.highlight .vc{color:#e5c07b}.highlight .vg{color:#e5c07b}.highlight .vi{color:#e06c75}.highlight .il{color:#d19a66}.highlight .gu{color:#75715e}.highlight .gd{color:#f92672}.highlight .gi{color:#a6e22e}.highlighter-rouge .highlight{margin-bottom:10px;border-radius:6px}.highlighter-rouge .highlight pre{font-size:14px;line-height:1.5;color:#555;background:0 0;border:0;margin:0;padding:0;word-wrap:normal}.highlighter-rouge .highlight .rouge-table .rouge-gutter,.highlighter-rouge .highlight .rouge-table .rouge-code{border:0!important}.highlighter-rouge .highlight .rouge-code pre{color:#abb2bf}.highlighter-rouge .highlight .table-responsive{margin:0;border:0}.highlighter-rouge .highlight .table{margin:0;table-layout:fixed}.highlighter-rouge .highlight table>tbody>tr>td{margin:0;border:0;padding:0}.highlighter-rouge .highlight table>tbody>tr>td>pre{padding:14px}.highlighter-rouge .highlight td.rouge-gutter{width:56px}.highlighter-rouge .highlight .lineno{text-align:right;border-radius:0}@media (max-width:480px){.highlighter-rouge .highlight{margin-left:-15px;margin-right:-15px;border-radius:0}.highlighter-rouge .highlight td.rouge-gutter{width:36px}.highlighter-rouge .highlight table>tbody>tr>td>pre{padding:14px 10px}}body{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:16px;color:#404040;overflow-x:hidden;text-rendering:auto;-webkit-font-smoothing:antialiased;-moz-osx-font-smoothing:grayscale}p{margin:30px 0}@media screen and (max-width:768px){p{margin:25px 0}}h1,h2,h3,h4,h5,h6{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;line-height:1.1;font-weight:700}h4{font-size:21px}a{color:#404040}a:hover,a:focus{color:#0085a1}a img:hover,a img:focus{cursor:zoom-in}article{overflow:hidden}blockquote{color:gray;font-style:italic;font-size:.95em;margin:20px 0 20px}blockquote p{margin:0}small.img-hint{display:block;margin-top:-20px;text-align:center}br+small.img-hint{margin-top:-40px}img.shadow{box-shadow:rgba(0,0,0,.258824) 0 2px 5px 0}select{-webkit-appearance:none;margin-top:15px;color:#337ab7;border-color:#337ab7;padding:0 .4em;background:#fff}select.sel-lang{min-height:28px;font-size:14px}table{margin-top:10px}table.table>tbody th,table.table>thead th,table.table>tbody td,table.table>thead td{border:1px solid #eee!important}@media screen and (max-width:767px){.table-responsive{border:0}}hr.small{max-width:100px;margin:15px auto;border-width:4px;border-color:#fff}pre,.table-responsive{-webkit-overflow-scrolling:touch}pre code{display:block;width:auto;white-space:pre;word-wrap:normal}code,kbd,pre,samp{font-family:"Fira Code",Menlo,Monaco,Consolas,"Courier New",monospace}.postlist-container{margin-bottom:15px}.post-container a{color:#337ab7}.post-container a:hover,.post-container a:focus{color:#0085a1}.post-container h1,.post-container h2,.post-container h3,.post-container h4,.post-container h5,.post-container h6{margin:50px 0 20px;line-height:1.4}.post-container h1+p,.post-container h2+p,.post-container h3+p,.post-container h4+p,.post-container h5+p,.post-container h6+p{margin-top:20px}.post-container h2::before{content:" ";display:block;border-bottom:1px solid #ececec;margin-top:44px;margin-bottom:30px}.post-container h4{font-size:19px;font-weight:600;color:gray}.post-container h4+p{margin-top:10px}.post-container h5,.post-container h6{font-size:17px;font-weight:600;color:gray}.post-container h5+p,.post-container h6+p{margin-top:10px}@media screen and (max-width:768px){.post-container h1{font-size:30px}.post-container h2{font-size:22px}.post-container h3{font-size:19px}.post-container h4{font-size:18px}}.post-container ul,.post-container ol{margin-bottom:40px}@media screen and (max-width:768px){.post-container ul,.post-container ol{padding-left:30px}}@media screen and (max-width:500px){.post-container ul,.post-container ol{padding-left:20px}}.post-container ol ol,.post-container ol ul,.post-container ul ol,.post-container ul ul{margin-bottom:5px}.post-container li p{margin:0;margin-bottom:5px}.post-container li h1,.post-container li h2,.post-container li h3,.post-container li h4,.post-container li h5,.post-container li h6{line-height:2;margin-top:20px}.post-container .pager li{width:48%}.post-container .pager li.next{float:right}.post-container .pager li.previous{float:left}.post-container .pager li>a{width:100%}.post-container .pager li>a>span{color:#ccc;font-weight:400;letter-spacing:.5px}.post-container .anchorjs-link{position:absolute;text-decoration:none!important}@media only screen and (max-width:767px){.navbar-default .navbar-collapse{position:absolute;right:0;border:none;background:#fff;box-shadow:0 5px 10px 2px rgba(0,0,0,.2);box-shadow:rgba(0,0,0,.117647) 0 1px 6px,rgba(0,0,0,.239216) 0 1px 4px;border-radius:2px;width:170px}#huxblog_navbar{opacity:0;transform:scaleX(0);transform-origin:top right;transition:all 200ms cubic-bezier(0.47,0,.4,.99) 0ms;-webkit-transform:scaleX(0);-webkit-transform-origin:top right;-webkit-transition:all 200ms cubic-bezier(0.47,0,.4,.99) 0ms}#huxblog_navbar a{font-size:13px;line-height:28px}#huxblog_navbar .navbar-collapse{height:0;transform:scaleY(0);transform-origin:top right;transition:transform 400ms cubic-bezier(0.32,1,.23,1) 0ms;-webkit-transform:scaleY(0);-webkit-transform-origin:top right;-webkit-transition:-webkit-transform 400ms cubic-bezier(0.32,1,.23,1) 0ms}#huxblog_navbar li{opacity:0;transition:opacity 100ms cubic-bezier(0.23,1,.32,1) 0ms;-webkit-transition:opacity 100ms cubic-bezier(0.23,1,.32,1) 0ms}#huxblog_navbar.in{transform:scaleX(1);-webkit-transform:scaleX(1);opacity:1;transition:all 250ms cubic-bezier(0.23,1,.32,1) 0ms;-webkit-transition:all 250ms cubic-bezier(0.23,1,.32,1) 0ms}#huxblog_navbar.in .navbar-collapse{transform:scaleY(1);-webkit-transform:scaleY(1);transition:transform 500ms cubic-bezier(0.23,1,.32,1);-webkit-transition:-webkit-transform 500ms cubic-bezier(0.23,1,.32,1)}#huxblog_navbar.in li{opacity:1;transition:opacity 450ms cubic-bezier(0.23,1,.32,1) 205ms;-webkit-transition:opacity 450ms cubic-bezier(0.23,1,.32,1) 205ms}}.navbar-custom{background:0 0;border:none;position:absolute;top:0;left:0;width:100%;z-index:3;font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7}.navbar-custom .navbar-brand{font-weight:800;color:#fff;height:56px;line-height:25px}.navbar-custom .navbar-brand:hover{color:rgba(255,255,255,.8)}.navbar-custom .nav li a{text-transform:uppercase;font-size:12px;line-height:20px;font-weight:800;letter-spacing:1px}.navbar-custom .nav li a:active{background:rgba(0,0,0,.12)}@media only screen and (min-width:768px){.navbar-custom{background:0 0;border-bottom:1px solid transparent}.navbar-custom body{font-size:20px}.navbar-custom .navbar-brand{color:#fff;padding:20px;line-height:20px}.navbar-custom .navbar-brand:hover,.navbar-custom .navbar-brand:focus{color:rgba(255,255,255,.8)}.navbar-custom .nav li a{color:#fff;padding:20px}.navbar-custom .nav li a:hover,.navbar-custom .nav li a:focus{color:rgba(255,255,255,.8)}.navbar-custom .nav li a:active{background:0 0}}.navbar-custom.invert .navbar-toggle:active{background-color:rgba(0,0,0,.05)}.navbar-custom.invert .navbar-toggle .icon-bar{background-color:#404040}.navbar-custom.invert .navbar-brand{color:#404040}.navbar-custom.invert .navbar-brand:hover,.navbar-custom.invert .navbar-brand:focus{color:#0085a1}.navbar-custom.invert .nav li a{color:#404040}.navbar-custom.invert .nav li a:hover,.navbar-custom.invert .nav li a:focus{color:#0085a1}@media only screen and (min-width:1170px){.navbar-custom{-webkit-transition:background-color .3s;-moz-transition:background-color .3s;transition:background-color .3s;-webkit-transform:translate3d(0,0,0);-moz-transform:translate3d(0,0,0);-ms-transform:translate3d(0,0,0);-o-transform:translate3d(0,0,0);transform:translate3d(0,0,0);-webkit-backface-visibility:hidden;backface-visibility:hidden}.navbar-custom.is-fixed{position:fixed;top:-61px;background-color:rgba(255,255,255,.9);border-bottom:1px solid #f2f2f2;-webkit-transition:-webkit-transform .3s;-moz-transition:-moz-transform .3s;transition:transform .3s}.navbar-custom.is-fixed .navbar-brand{color:#404040}.navbar-custom.is-fixed .navbar-brand:hover,.navbar-custom.is-fixed .navbar-brand:focus{color:#0085a1}.navbar-custom.is-fixed .nav li a{color:#404040}.navbar-custom.is-fixed .nav li a:hover,.navbar-custom.is-fixed .nav li a:focus{color:#0085a1}.navbar-custom.is-visible{-webkit-transform:translate3d(0,100%,0);-moz-transform:translate3d(0,100%,0);-ms-transform:translate3d(0,100%,0);-o-transform:translate3d(0,100%,0);transform:translate3d(0,100%,0)}}.intro-header{background:no-repeat center center;background-color:#ccc;background-attachment:scroll;-webkit-background-size:cover;-moz-background-size:cover;background-size:cover;-o-background-size:cover;margin-bottom:0}.intro-header.style-text{background:0 0}.intro-header.style-text .site-heading,.intro-header.style-text .post-heading,.intro-header.style-text .page-heading{padding:85px 0 20px;color:#404040}.intro-header.style-text .site-heading .subheading,.intro-header.style-text .post-heading .subheading,.intro-header.style-text .page-heading .subheading{margin-bottom:15px}.intro-header.style-text .tags a,.intro-header.style-text .tags .tag{border-color:#404040;color:#404040}.intro-header.style-text .tags a:hover,.intro-header.style-text .tags .tag:hover,.intro-header.style-text .tags a:active,.intro-header.style-text .tags .tag:active{background-color:rgba(0,0,0,.05)}@media only screen and (min-width:768px){.intro-header{margin-bottom:20px}}.intro-header .site-heading,.intro-header .post-heading,.intro-header .page-heading{padding:85px 0 55px;color:#fff}@media only screen and (min-width:768px){.intro-header .site-heading,.intro-header .post-heading,.intro-header .page-heading{padding:150px 0}}.intro-header .site-heading{padding:95px 0 70px}@media only screen and (min-width:768px){.intro-header .site-heading{padding:150px 0}}.intro-header .site-heading,.intro-header .page-heading{text-align:center}.intro-header .site-heading h1,.intro-header .page-heading h1{margin-top:0;font-size:50px}.intro-header .site-heading .subheading,.intro-header .page-heading .subheading{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:18px;line-height:1.1;display:block;font-weight:300;margin:10px 0 0}@media only screen and (min-width:768px){.intro-header .site-heading h1,.intro-header .page-heading h1{font-size:80px}}.intro-header .post-heading h1{font-size:30px;margin-bottom:24px}.intro-header .post-heading .subheading,.intro-header .post-heading .meta{line-height:1.1;display:block}.intro-header .post-heading .subheading{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:17px;line-height:1.4;font-weight:400;margin:10px 0 30px;margin-top:-5px}.intro-header .post-heading .meta{font-family:Lora,'Times New Roman',serif;font-style:italic;font-weight:300;font-size:16px}.intro-header .post-heading .meta a{color:#fff}@media only screen and (min-width:768px){.intro-header .post-heading h1{font-size:55px}.intro-header .post-heading .subheading{font-size:30px}.intro-header .post-heading .meta{font-size:20px}}.intro-header .header-img-credit{position:absolute;bottom:6px;right:9px;color:#fff;opacity:.3;font-size:10px;z-index:1}.intro-header .header-img-credit a{color:#fff}@media only screen and (min-width:768px){.intro-header .header-img-credit{font-size:12px;bottom:10px;right:15px}}.post-preview>a{color:#404040}.post-preview>a:hover,.post-preview>a:focus{text-decoration:none;color:#0085a1}.post-preview>a>.post-title{font-size:21px;line-height:1.3;margin-top:30px;margin-bottom:8px}.post-preview>a>.post-subtitle{font-size:15px;line-height:1.3;margin:0;font-weight:300;margin-bottom:10px}.post-preview>.post-meta{font-family:Lora,'Times New Roman',serif;color:#ccc;font-size:16px;font-style:italic;margin-top:0}.post-preview>.post-meta>a{text-decoration:none;color:#404040}.post-preview>.post-meta>a:hover,.post-preview>.post-meta>a:focus{color:#0085a1;text-decoration:underline}@media only screen and (min-width:768px){.post-preview>a>.post-title{font-size:26px;line-height:1.3;margin-bottom:10px}.post-preview>a>.post-subtitle{font-size:16px}.post-preview .post-meta{font-size:18px}}.post-content-preview{font-size:13px;font-style:italic;color:#a3a3a3}.post-content-preview:hover{color:#0085a1}@media only screen and (min-width:768px){.post-content-preview{font-size:14px}}.section-heading{font-size:36px;margin-top:60px;font-weight:700}.caption{text-align:center;font-size:14px;padding:10px;font-style:italic;margin:0;display:block;border-bottom-right-radius:5px;border-bottom-left-radius:5px}footer{font-size:20px;padding:50px 0 65px}footer .list-inline{margin:0;padding:0}footer .copyright{font-size:14px;text-align:center;margin-bottom:0}footer .copyright a{color:#337ab7}footer .copyright a:hover,footer .copyright a:focus{color:#0085a1}.floating-label-form-group{font-size:14px;position:relative;margin-bottom:0;padding-bottom:.5em;border-bottom:1px solid #eee}.floating-label-form-group input,.floating-label-form-group textarea{z-index:1;position:relative;padding-right:0;padding-left:0;border:none;border-radius:0;font-size:1.5em;background:0 0;box-shadow:none!important;resize:none}.floating-label-form-group label{display:block;z-index:0;position:relative;top:2em;margin:0;font-size:.85em;line-height:1.764705882em;vertical-align:middle;vertical-align:baseline;opacity:0;-webkit-transition:top .3s ease,opacity .3s ease;-moz-transition:top .3s ease,opacity .3s ease;-ms-transition:top .3s ease,opacity .3s ease;transition:top .3s ease,opacity .3s ease}.floating-label-form-group::not(:first-child){padding-left:14px;border-left:1px solid #eee}.floating-label-form-group-with-value label{top:0;opacity:1}.floating-label-form-group-with-focus label{color:#0085a1}form .row:first-child .floating-label-form-group{border-top:1px solid #eee}.btn{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;text-transform:uppercase;font-size:14px;font-weight:800;letter-spacing:1px;border-radius:0;padding:15px 25px}.btn-lg{font-size:16px;padding:25px 35px}.btn-default:hover,.btn-default:focus{background-color:#0085a1;border:1px solid #0085a1;color:#fff}.pager{margin:20px 0 0!important;padding:0!important}.pager li>a,.pager li>span{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;text-transform:uppercase;font-size:13px;font-weight:800;letter-spacing:1px;padding:10px;background-color:#fff;border-radius:0}@media only screen and (min-width:768px){.pager li>a,.pager li>span{font-size:14px;padding:15px 25px}}.pager li>a{color:#404040}.pager li>a:hover,.pager li>a:focus{color:#fff;background-color:#0085a1;border:1px solid #0085a1}.pager li>a:hover>span,.pager li>a:focus>span{color:#fff}.pager .disabled>a,.pager .disabled>a:hover,.pager .disabled>a:focus,.pager .disabled>span{color:#ccc;background-color:#404040;cursor:not-allowed}::-moz-selection{color:#fff;text-shadow:none;background:#0085a1}::selection{color:#fff;text-shadow:none;background:#0085a1}img::selection{color:#fff;background:0 0}img::-moz-selection{color:#fff;background:0 0}.d-none{display:none!important}.tags{margin-bottom:-5px}.tags.tags-sup a,.tags.tags-sup .tag{padding:0 10px 0 12px}.tags a,.tags .tag{display:inline-block;border:1px solid rgba(255,255,255,.8);border-radius:999em;padding:0 10px 0 10px;color:#fff;line-height:24px;font-size:12px;text-decoration:none;margin:0 1px;margin-bottom:6px;cursor:pointer}.tags a>sup,.tags .tag>sup{margin-left:-2px;font-weight:700}.tags a:hover,.tags .tag:hover,.tags a:active,.tags .tag:active{color:#fff;border-color:#fff;background-color:rgba(255,255,255,.4);text-decoration:none}@media only screen and (min-width:768px){.tags a,.tags .tag{margin-right:5px}}#tag-heading{padding:70px 0 60px}@media only screen and (min-width:768px){#tag-heading{padding:55px 0}}#tag_cloud{margin:20px 0 15px 0}#tag_cloud a,#tag_cloud .tag{transition-property:all;transition-duration:.4s;transition-timing-function:ease;font-size:14px;border:none;line-height:28px;margin:0 2px;margin-bottom:8px;background:#f3f5f5}#tag_cloud a:hover,#tag_cloud .tag:hover,#tag_cloud a:active,#tag_cloud .tag:active,#tag_cloud a.focus,#tag_cloud .tag.focus{background-color:#0085a1!important}#tag_cloud a.focus,#tag_cloud .tag.focus{box-shadow:rgba(0,0,0,.117647) 0 1px 6px,rgba(0,0,0,.239216) 0 1px 4px}#tag_cloud a.tag-button--all,#tag_cloud .tag.tag-button--all{font-weight:700;color:#0085a1!important}#tag_cloud a.tag-button--all:hover,#tag_cloud .tag.tag-button--all:hover,#tag_cloud a.tag-button--all:active,#tag_cloud .tag.tag-button--all:active,#tag_cloud a.tag-button--all.focus,#tag_cloud .tag.tag-button--all.focus{background-color:#e4e4e4!important}@media only screen and (min-width:768px){#tag_cloud{margin-bottom:25px}}.tag-comments{font-size:12px}@media only screen and (min-width:768px){.tag-comments{font-size:14px}}.t:first-child{margin-top:0}.listing-seperator{color:#0085a1;font-size:21px!important}.listing-seperator::before{margin-right:5px}@media only screen and (min-width:768px){.listing-seperator{font-size:20px!important;line-height:2!important}}.mini-post-list{margin:20px 0 15px 0}.mini-post-list .tag-text{font-weight:200;font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7}.mini-post-list .post-preview{position:relative}.mini-post-list .post-preview>a .post-title{font-size:16px;font-weight:500;margin-top:20px}.mini-post-list .post-preview>a .post-subtitle{font-size:13px}.mini-post-list .post-preview>.post-meta{position:absolute;right:5px;bottom:0;margin:0;font-size:12px;line-height:12px}@media only screen and (min-width:768px){.mini-post-list .post-preview{margin-left:20px}.mini-post-list .post-preview>a>.post-title{font-size:18px;line-height:1.3}.mini-post-list .post-preview>a>.post-subtitle{font-size:14px}.mini-post-list .post-preview .post-meta{font-size:18px}}.post-container img{display:block;max-width:100%;height:auto;margin:1.5em auto 1.6em auto}.navbar-default .navbar-toggle:focus,.navbar-default .navbar-toggle:hover{background-color:inherit}.navbar-default .navbar-toggle:active{background-color:rgba(255,255,255,.25)}.navbar-default .navbar-toggle{border-color:transparent;padding:19px 16px;margin-top:2px;margin-right:2px;margin-bottom:2px;border-radius:50%}.navbar-default .navbar-toggle .icon-bar{width:18px;border-radius:0;background-color:#fff}.navbar-default .navbar-toggle .icon-bar+.icon-bar{margin-top:3px}.comment{margin-top:20px}.comment #ds-thread #ds-reset a.ds-like-thread-button{border:1px solid #ddd;border-radius:0;background:#fff;box-shadow:none;text-shadow:none}.comment #ds-thread #ds-reset li.ds-tab a.ds-current{border:1px solid #ddd;border-radius:0;background:#fff;box-shadow:none;text-shadow:none}.comment #ds-thread #ds-reset .ds-textarea-wrapper{background:0 0}.comment #ds-thread #ds-reset .ds-gradient-bg{background:0 0}.comment #ds-thread #ds-reset .ds-post-options{border-bottom:1px solid #ccc}.comment #ds-thread #ds-reset .ds-post-button{border-bottom:1px solid #ccc}.comment #ds-thread #ds-reset .ds-post-button{background:#fff;box-shadow:none}.comment #ds-thread #ds-reset .ds-post-button:hover{background:#eee}#ds-smilies-tooltip ul.ds-smilies-tabs li a{background:#fff!important}.page-fullscreen .intro-header{position:fixed;left:0;top:0;width:100%;height:100%}.page-fullscreen #tag-heading{position:fixed;left:0;top:0;padding-bottom:150px;width:100%;height:100%;display:-webkit-box;-webkit-box-orient:vertical;-webkit-box-pack:center;-webkit-box-align:center;display:-webkit-flex;-webkit-align-items:center;-webkit-justify-content:center;-webkit-flex-direction:column;display:flex;align-items:center;justify-content:center;flex-direction:column}.page-fullscreen footer{position:absolute;width:100%;bottom:0;padding-bottom:20px;opacity:.6;color:#fff}.page-fullscreen footer .copyright{color:#fff}.page-fullscreen footer .copyright a{color:#fff}.page-fullscreen footer .copyright a:hover{color:#ddd}.MathJax_SVG_Display{overflow:auto;-webkit-overflow-scrolling:touch}
\ No newline at end of file
+@media (min-width:1200px){.post-container,.sidebar-container{padding-right:5%}}@media (min-width:768px){.post-container{padding-right:5%}}.sidebar-container{color:#bfbfbf;font-size:14px}.sidebar-container h5{color:#ccc;padding-bottom:1em}.sidebar-container h5 a{color:#ccc!important;text-decoration:none}.sidebar-container a{color:#bfbfbf!important}.sidebar-container a:hover,.sidebar-container a:active{color:#0085a1!important}.sidebar-container .tags a{border-color:#bfbfbf}.sidebar-container .tags a:hover,.sidebar-container .tags a:active{border-color:#0085a1}.sidebar-container .short-about img{width:80%;display:block;border-radius:5px;margin-bottom:20px}.sidebar-container .short-about p{margin-top:0;margin-bottom:20px}.sidebar-container .short-about .list-inline>li{padding-left:0}.catalog-container{padding:0}.side-catalog{display:block;overflow:auto;height:100%;padding-bottom:40px;width:195px}.side-catalog.fixed{position:fixed;top:-21px}.side-catalog.fold .catalog-toggle::before{content:"+"}.side-catalog.fold .catalog-body{display:none}.side-catalog .catalog-toggle::before{content:"−";position:relative;margin-right:5px;bottom:1px}.side-catalog .catalog-body{position:relative;list-style:none;height:auto;overflow:hidden;padding-left:0;padding-right:5px;text-indent:0}.side-catalog .catalog-body li{position:relative;list-style:none}.side-catalog .catalog-body li a{padding-left:10px;max-width:180px;display:inline-block;vertical-align:middle;height:30px;line-height:30px;overflow:hidden;text-decoration:none;white-space:nowrap;text-overflow:ellipsis}.side-catalog .catalog-body .h1_nav,.side-catalog .catalog-body .h2_nav,.side-catalog .catalog-body .h3_nav{margin-left:0;font-size:13px;font-weight:700}.side-catalog .catalog-body .h4_nav,.side-catalog .catalog-body .h5_nav,.side-catalog .catalog-body .h6_nav{margin-left:10px;font-size:12px}.side-catalog .catalog-body .h4_nav a,.side-catalog .catalog-body .h5_nav a,.side-catalog .catalog-body .h6_nav a{max-width:170px}.side-catalog .catalog-body .active{border-radius:4px;background-color:#F5F5F5}.side-catalog .catalog-body .active a{color:#0085a1!important}@media (max-width:1200px){.side-catalog{display:none}}.paper-snackbar{transition-property:opacity,bottom,left,right,width,margin,border-radius;transition-duration:.5s;transition-timing-function:ease;font-size:14px;min-height:14px;background-color:#323232;background-color:#0085a1;position:fixed;display:flex;justify-content:space-between;align-items:center;color:#fff;line-height:22px;padding:18px 24px;bottom:0;opacity:0}@media (min-width:640px){.paper-snackbar{min-width:288px;max-width:568px;display:inline-flex;border-radius:2px;margin:24px;bottom:-100px}}@media (max-width:640px){.paper-snackbar{left:0;right:0}}.paper-snackbar .action{background:inherit;display:inline-block;border:none;font-size:inherit;text-transform:uppercase;color:#ffeb3b;margin:0 0 0 24px;padding:0;min-width:min-content;outline:0}.paper-button{position:relative;padding:4px 0;margin:1em;width:160px;overflow:hidden;user-select:none;color:#000;text-transform:uppercase;border-radius:3px;outline-color:#ccc}.paper-button:hover{cursor:pointer}.paper-button button,.paper-button input[type=submit]{background:inherit;border:none;display:block;width:100%;height:100%;font-size:1em;color:#000;text-transform:uppercase}.paper-button.colored,.paper-button.colored button{color:#4285f4}.paper-button.raised-button.colored{background-color:#4285f4}.paper-button .raised-button{box-shadow:0 2px 5px 0 rgba(0,0,0,.26)}.paper-button.raised-button.colored{background:#4285f4;color:#fff}.paper-button[disabled]{background-color:#EAEAEA!important;color:#A8A8A8!important;cursor:auto}.paper-button:hover{background-color:#EAEAEA}.paper-button.raised-button.colored:hover{background-color:#3367d6}button.paper-button{border:0;font-size:1em;line-height:25px;background-color:#fff}.paper-button input[type=submit]{outline-color:#ccc}.paper-button.colored.raised-button input[type=submit]{color:#fff}.paper-shadow-animated.paper-shadow{transition:box-shadow .28s cubic-bezier(0.4,0,.2,1)}.paper-shadow-top-z-1{box-shadow:0 2px 10px 0 rgba(0,0,0,.16)}.paper-shadow-bottom-z-1{box-shadow:0 2px 5px 0 rgba(0,0,0,.26)}.paper-shadow-top-z-2{box-shadow:0 6px 20px 0 rgba(0,0,0,.19)}.paper-shadow-bottom-z-2{box-shadow:0 8px 17px 0 rgba(0,0,0,.2)}.paper-shadow-top-z-3{box-shadow:0 17px 50px 0 rgba(0,0,0,.19)}.paper-shadow-bottom-z-3{box-shadow:0 12px 15px 0 rgba(0,0,0,.24)}.paper-shadow-top-z-4{box-shadow:0 25px 55px 0 rgba(0,0,0,.21)}.card{background:#fff;width:300px;height:300px;position:relative;margin:16px;border-radius:2px}.highlight,pre.highlight{background:#282c34;color:#abb2bf}.highlight pre{background:#282c34}.highlight .hll{background:#282c34}.highlight .c{color:#5c6370;font-style:italic}.highlight .err{color:#960050;background-color:#1e0010}.language-coq .highlight .err{background-color:transparent}.highlight .k,.language-coq .highlight .err{color:#c678dd}.highlight .l{color:#98c379}.highlight .n{color:#abb2bf}.highlight .o{color:#abb2bf}.highlight .p{color:#abb2bf}.highlight .cm{color:#5c6370;font-style:italic}.highlight .cp{color:#5c6370;font-style:italic}.highlight .c1{color:#5c6370;font-style:italic}.highlight .cs{color:#5c6370;font-style:italic}.highlight .ge{font-style:italic}.highlight .gs{font-weight:700}.highlight .kc{color:#c678dd}.highlight .kd{color:#c678dd}.highlight .kn{color:#c678dd}.highlight .kp{color:#c678dd}.highlight .kr{color:#c678dd}.highlight .kt{color:#c678dd}.highlight .ld{color:#98c379}.highlight .m{color:#d19a66}.highlight .s{color:#98c379}.highlight .na{color:#d19a66}.highlight .nb{color:#e5c07b}.highlight .nc{color:#e5c07b}.highlight .no{color:#e5c07b}.highlight .nd{color:#e5c07b}.highlight .ni{color:#e5c07b}.highlight .ne{color:#e5c07b}.highlight .nf{color:#abb2bf}.highlight .nl{color:#e5c07b}.highlight .nn{color:#abb2bf}.highlight .nx{color:#abb2bf}.highlight .py{color:#e5c07b}.highlight .nt{color:#e06c75}.highlight .nv{color:#e5c07b}.highlight .ow{font-weight:700}.highlight .w{color:#f8f8f2}.highlight .mf{color:#d19a66}.highlight .mh{color:#d19a66}.highlight .mi{color:#d19a66}.highlight .mo{color:#d19a66}.highlight .sb{color:#98c379}.highlight .sc{color:#98c379}.highlight .sd{color:#98c379}.highlight .s2{color:#98c379}.highlight .se{color:#98c379}.highlight .sh{color:#98c379}.highlight .si{color:#98c379}.highlight .sx{color:#98c379}.highlight .sr{color:#56b6c2}.highlight .s1{color:#98c379}.highlight .ss{color:#56b6c2}.highlight .bp{color:#e5c07b}.highlight .vc{color:#e5c07b}.highlight .vg{color:#e5c07b}.highlight .vi{color:#e06c75}.highlight .il{color:#d19a66}.highlight .gu{color:#75715e}.highlight .gd{color:#f92672}.highlight .gi{color:#a6e22e}.highlighter-rouge .highlight{margin-bottom:10px;border-radius:6px}.highlighter-rouge .highlight pre{font-size:14px;line-height:1.5;color:#555;background:0 0;border:0;margin:0;padding:0;word-wrap:normal}.highlighter-rouge .highlight .rouge-table .rouge-gutter,.highlighter-rouge .highlight .rouge-table .rouge-code{border:0!important}.highlighter-rouge .highlight .rouge-code pre{color:#abb2bf}.highlighter-rouge .highlight .table-responsive{margin:0;border:0}.highlighter-rouge .highlight .table{margin:0;table-layout:fixed}.highlighter-rouge .highlight table>tbody>tr>td{margin:0;border:0;padding:0}.highlighter-rouge .highlight table>tbody>tr>td>pre{padding:14px}.highlighter-rouge .highlight td.rouge-gutter{width:56px}.highlighter-rouge .highlight .lineno{text-align:right;border-radius:0}@media (max-width:480px){.highlighter-rouge .highlight{margin-left:-15px;margin-right:-15px;border-radius:0}.highlighter-rouge .highlight td.rouge-gutter{width:36px}.highlighter-rouge .highlight table>tbody>tr>td>pre{padding:14px 10px}}body{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:16px;color:#404040;overflow-x:hidden;text-rendering:auto;-webkit-font-smoothing:antialiased;-moz-osx-font-smoothing:grayscale}p{margin:30px 0}@media screen and (max-width:768px){p{margin:25px 0}}h1,h2,h3,h4,h5,h6{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;line-height:1.1;font-weight:700}h4{font-size:21px}a{color:#404040}a:hover,a:focus{color:#0085a1}a img:hover,a img:focus{cursor:zoom-in}article{overflow:hidden}blockquote{color:gray;font-style:italic;font-size:.95em;margin:20px 0 20px}blockquote p{margin:0}small.img-hint{display:block;margin-top:-20px;text-align:center}br+small.img-hint{margin-top:-40px}img.shadow{box-shadow:rgba(0,0,0,.258824) 0 2px 5px 0}select{-webkit-appearance:none;margin-top:15px;color:#337ab7;border-color:#337ab7;padding:0 .4em;background:#fff}select.sel-lang{min-height:28px;font-size:14px}table{margin-top:10px}table.table>tbody th,table.table>thead th,table.table>tbody td,table.table>thead td{border:1px solid #eee!important}@media screen and (max-width:767px){.table-responsive{border:0}}hr.small{max-width:100px;margin:15px auto;border-width:4px;border-color:#fff}pre,.table-responsive{-webkit-overflow-scrolling:touch}pre code{display:block;width:auto;white-space:pre;word-wrap:normal}code,kbd,pre,samp{font-family:"Fira Code",Menlo,Monaco,Consolas,"Courier New",monospace}.postlist-container{margin-bottom:15px}.post-container a{color:#337ab7}.post-container a:hover,.post-container a:focus{color:#0085a1}.post-container h1,.post-container h2,.post-container h3,.post-container h4,.post-container h5,.post-container h6{margin:50px 0 20px;line-height:1.4}.post-container h1+p,.post-container h2+p,.post-container h3+p,.post-container h4+p,.post-container h5+p,.post-container h6+p{margin-top:20px}.post-container h2::before{content:" ";display:block;border-bottom:1px solid #ececec;margin-top:44px;margin-bottom:30px}.post-container h4{font-size:22px;font-weight:600;color:gray}.post-container h4+p{margin-top:10px}.post-container h5,.post-container h6{font-size:20px;font-weight:600;color:gray}.post-container h5+p,.post-container h6+p{margin-top:10px}@media screen and (max-width:768px){.post-container h1{font-size:30px}.post-container h2{font-size:22px}.post-container h3{font-size:20px}.post-container h4{font-size:19px}.post-container h5,.post-container h6{font-size:18px}}.post-container ul,.post-container ol{margin-bottom:40px}@media screen and (max-width:768px){.post-container ul,.post-container ol{padding-left:30px}}@media screen and (max-width:500px){.post-container ul,.post-container ol{padding-left:20px}}.post-container ol ol,.post-container ol ul,.post-container ul ol,.post-container ul ul{margin-bottom:5px}.post-container li p{margin:0;margin-bottom:5px}.post-container li h1,.post-container li h2,.post-container li h3,.post-container li h4,.post-container li h5,.post-container li h6{line-height:2;margin-top:20px}.post-container .pager li{width:48%}.post-container .pager li.next{float:right}.post-container .pager li.previous{float:left}.post-container .pager li>a{width:100%}.post-container .pager li>a>span{color:#ccc;font-weight:400;letter-spacing:.5px}.post-container .anchorjs-link{position:absolute;text-decoration:none!important}@media only screen and (max-width:767px){.navbar-default .navbar-collapse{position:absolute;right:0;border:none;background:#fff;box-shadow:0 5px 10px 2px rgba(0,0,0,.2);box-shadow:rgba(0,0,0,.117647) 0 1px 6px,rgba(0,0,0,.239216) 0 1px 4px;border-radius:2px;width:170px}#huxblog_navbar{opacity:0;transform:scaleX(0);transform-origin:top right;transition:all 200ms cubic-bezier(0.47,0,.4,.99) 0ms;-webkit-transform:scaleX(0);-webkit-transform-origin:top right;-webkit-transition:all 200ms cubic-bezier(0.47,0,.4,.99) 0ms}#huxblog_navbar a{font-size:13px;line-height:28px}#huxblog_navbar .navbar-collapse{height:0;transform:scaleY(0);transform-origin:top right;transition:transform 400ms cubic-bezier(0.32,1,.23,1) 0ms;-webkit-transform:scaleY(0);-webkit-transform-origin:top right;-webkit-transition:-webkit-transform 400ms cubic-bezier(0.32,1,.23,1) 0ms}#huxblog_navbar li{opacity:0;transition:opacity 100ms cubic-bezier(0.23,1,.32,1) 0ms;-webkit-transition:opacity 100ms cubic-bezier(0.23,1,.32,1) 0ms}#huxblog_navbar.in{transform:scaleX(1);-webkit-transform:scaleX(1);opacity:1;transition:all 250ms cubic-bezier(0.23,1,.32,1) 0ms;-webkit-transition:all 250ms cubic-bezier(0.23,1,.32,1) 0ms}#huxblog_navbar.in .navbar-collapse{transform:scaleY(1);-webkit-transform:scaleY(1);transition:transform 500ms cubic-bezier(0.23,1,.32,1);-webkit-transition:-webkit-transform 500ms cubic-bezier(0.23,1,.32,1)}#huxblog_navbar.in li{opacity:1;transition:opacity 450ms cubic-bezier(0.23,1,.32,1) 205ms;-webkit-transition:opacity 450ms cubic-bezier(0.23,1,.32,1) 205ms}}.navbar-custom{background:0 0;border:none;position:absolute;top:0;left:0;width:100%;z-index:3;font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7}.navbar-custom .navbar-brand{font-weight:800;color:#fff;height:56px;line-height:25px}.navbar-custom .navbar-brand:hover{color:rgba(255,255,255,.8)}.navbar-custom .nav li a{text-transform:uppercase;font-size:12px;line-height:20px;font-weight:800;letter-spacing:1px}.navbar-custom .nav li a:active{background:rgba(0,0,0,.12)}@media only screen and (min-width:768px){.navbar-custom{background:0 0;border-bottom:1px solid transparent}.navbar-custom body{font-size:20px}.navbar-custom .navbar-brand{color:#fff;padding:20px;line-height:20px}.navbar-custom .navbar-brand:hover,.navbar-custom .navbar-brand:focus{color:rgba(255,255,255,.8)}.navbar-custom .nav li a{color:#fff;padding:20px}.navbar-custom .nav li a:hover,.navbar-custom .nav li a:focus{color:rgba(255,255,255,.8)}.navbar-custom .nav li a:active{background:0 0}}.navbar-custom.invert .navbar-toggle:active{background-color:rgba(0,0,0,.05)}.navbar-custom.invert .navbar-toggle .icon-bar{background-color:#404040}.navbar-custom.invert .navbar-brand{color:#404040}.navbar-custom.invert .navbar-brand:hover,.navbar-custom.invert .navbar-brand:focus{color:#0085a1}.navbar-custom.invert .nav li a{color:#404040}.navbar-custom.invert .nav li a:hover,.navbar-custom.invert .nav li a:focus{color:#0085a1}@media only screen and (min-width:1170px){.navbar-custom{-webkit-transition:background-color .3s;-moz-transition:background-color .3s;transition:background-color .3s;-webkit-transform:translate3d(0,0,0);-moz-transform:translate3d(0,0,0);-ms-transform:translate3d(0,0,0);-o-transform:translate3d(0,0,0);transform:translate3d(0,0,0);-webkit-backface-visibility:hidden;backface-visibility:hidden}.navbar-custom.is-fixed{position:fixed;top:-61px;background-color:rgba(255,255,255,.9);border-bottom:1px solid #f2f2f2;-webkit-transition:-webkit-transform .3s;-moz-transition:-moz-transform .3s;transition:transform .3s}.navbar-custom.is-fixed .navbar-brand{color:#404040}.navbar-custom.is-fixed .navbar-brand:hover,.navbar-custom.is-fixed .navbar-brand:focus{color:#0085a1}.navbar-custom.is-fixed .nav li a{color:#404040}.navbar-custom.is-fixed .nav li a:hover,.navbar-custom.is-fixed .nav li a:focus{color:#0085a1}.navbar-custom.is-visible{-webkit-transform:translate3d(0,100%,0);-moz-transform:translate3d(0,100%,0);-ms-transform:translate3d(0,100%,0);-o-transform:translate3d(0,100%,0);transform:translate3d(0,100%,0)}}.intro-header{background:no-repeat center center;background-color:#ccc;background-attachment:scroll;-webkit-background-size:cover;-moz-background-size:cover;background-size:cover;-o-background-size:cover;margin-bottom:0}.intro-header.style-text{background:0 0}.intro-header.style-text .site-heading,.intro-header.style-text .post-heading,.intro-header.style-text .page-heading{padding:85px 0 20px;color:#404040}.intro-header.style-text .site-heading .subheading,.intro-header.style-text .post-heading .subheading,.intro-header.style-text .page-heading .subheading{margin-bottom:15px}.intro-header.style-text .tags a,.intro-header.style-text .tags .tag{border-color:#404040;color:#404040}.intro-header.style-text .tags a:hover,.intro-header.style-text .tags .tag:hover,.intro-header.style-text .tags a:active,.intro-header.style-text .tags .tag:active{background-color:rgba(0,0,0,.05)}@media only screen and (min-width:768px){.intro-header{margin-bottom:20px}}.intro-header .site-heading,.intro-header .post-heading,.intro-header .page-heading{padding:85px 0 55px;color:#fff}@media only screen and (min-width:768px){.intro-header .site-heading,.intro-header .post-heading,.intro-header .page-heading{padding:150px 0}}.intro-header .site-heading{padding:95px 0 70px}@media only screen and (min-width:768px){.intro-header .site-heading{padding:150px 0}}.intro-header .site-heading,.intro-header .page-heading{text-align:center}.intro-header .site-heading h1,.intro-header .page-heading h1{margin-top:0;font-size:50px}.intro-header .site-heading .subheading,.intro-header .page-heading .subheading{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:18px;line-height:1.1;display:block;font-weight:300;margin:10px 0 0}@media only screen and (min-width:768px){.intro-header .site-heading h1,.intro-header .page-heading h1{font-size:80px}}.intro-header .post-heading h1{font-size:30px;margin-bottom:24px}.intro-header .post-heading .subheading,.intro-header .post-heading .meta{line-height:1.1;display:block}.intro-header .post-heading .subheading{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;font-size:17px;line-height:1.4;font-weight:400;margin:10px 0 30px;margin-top:-5px}.intro-header .post-heading .meta{font-family:Lora,'Times New Roman',serif;font-style:italic;font-weight:300;font-size:16px}.intro-header .post-heading .meta a{color:#fff}@media only screen and (min-width:768px){.intro-header .post-heading h1{font-size:55px}.intro-header .post-heading .subheading{font-size:30px}.intro-header .post-heading .meta{font-size:20px}}.intro-header .header-img-credit{position:absolute;bottom:6px;right:9px;color:#fff;opacity:.3;font-size:10px;z-index:1}.intro-header .header-img-credit a{color:#fff}@media only screen and (min-width:768px){.intro-header .header-img-credit{font-size:12px;bottom:10px;right:15px}}.post-preview>a{color:#404040}.post-preview>a:hover,.post-preview>a:focus{text-decoration:none;color:#0085a1}.post-preview>a>.post-title{font-size:21px;line-height:1.3;margin-top:30px;margin-bottom:8px}.post-preview>a>.post-subtitle{font-size:15px;line-height:1.3;margin:0;font-weight:300;margin-bottom:10px}.post-preview>.post-meta{font-family:Lora,'Times New Roman',serif;color:#ccc;font-size:16px;font-style:italic;margin-top:0}.post-preview>.post-meta>a{text-decoration:none;color:#404040}.post-preview>.post-meta>a:hover,.post-preview>.post-meta>a:focus{color:#0085a1;text-decoration:underline}@media only screen and (min-width:768px){.post-preview>a>.post-title{font-size:26px;line-height:1.3;margin-bottom:10px}.post-preview>a>.post-subtitle{font-size:16px}.post-preview .post-meta{font-size:18px}}.post-content-preview{font-size:13px;font-style:italic;color:#a3a3a3}.post-content-preview:hover{color:#0085a1}@media only screen and (min-width:768px){.post-content-preview{font-size:14px}}.section-heading{font-size:36px;margin-top:60px;font-weight:700}.caption{text-align:center;font-size:14px;padding:10px;font-style:italic;margin:0;display:block;border-bottom-right-radius:5px;border-bottom-left-radius:5px}footer{font-size:20px;padding:50px 0 65px}footer .list-inline{margin:0;padding:0}footer .copyright{font-size:14px;text-align:center;margin-bottom:0}footer .copyright a{color:#337ab7}footer .copyright a:hover,footer .copyright a:focus{color:#0085a1}.floating-label-form-group{font-size:14px;position:relative;margin-bottom:0;padding-bottom:.5em;border-bottom:1px solid #eee}.floating-label-form-group input,.floating-label-form-group textarea{z-index:1;position:relative;padding-right:0;padding-left:0;border:none;border-radius:0;font-size:1.5em;background:0 0;box-shadow:none!important;resize:none}.floating-label-form-group label{display:block;z-index:0;position:relative;top:2em;margin:0;font-size:.85em;line-height:1.764705882em;vertical-align:middle;vertical-align:baseline;opacity:0;-webkit-transition:top .3s ease,opacity .3s ease;-moz-transition:top .3s ease,opacity .3s ease;-ms-transition:top .3s ease,opacity .3s ease;transition:top .3s ease,opacity .3s ease}.floating-label-form-group::not(:first-child){padding-left:14px;border-left:1px solid #eee}.floating-label-form-group-with-value label{top:0;opacity:1}.floating-label-form-group-with-focus label{color:#0085a1}form .row:first-child .floating-label-form-group{border-top:1px solid #eee}.btn{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;text-transform:uppercase;font-size:14px;font-weight:800;letter-spacing:1px;border-radius:0;padding:15px 25px}.btn-lg{font-size:16px;padding:25px 35px}.btn-default:hover,.btn-default:focus{background-color:#0085a1;border:1px solid #0085a1;color:#fff}.pager{margin:20px 0 0!important;padding:0!important}.pager li>a,.pager li>span{font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7;text-transform:uppercase;font-size:13px;font-weight:800;letter-spacing:1px;padding:10px;background-color:#fff;border-radius:0}@media only screen and (min-width:768px){.pager li>a,.pager li>span{font-size:14px;padding:15px 25px}}.pager li>a{color:#404040}.pager li>a:hover,.pager li>a:focus{color:#fff;background-color:#0085a1;border:1px solid #0085a1}.pager li>a:hover>span,.pager li>a:focus>span{color:#fff}.pager .disabled>a,.pager .disabled>a:hover,.pager .disabled>a:focus,.pager .disabled>span{color:#ccc;background-color:#404040;cursor:not-allowed}::-moz-selection{color:#fff;text-shadow:none;background:#0085a1}::selection{color:#fff;text-shadow:none;background:#0085a1}img::selection{color:#fff;background:0 0}img::-moz-selection{color:#fff;background:0 0}.d-none{display:none!important}.tags{margin-bottom:-5px}.tags.tags-sup a,.tags.tags-sup .tag{padding:0 10px 0 12px}.tags a,.tags .tag{display:inline-block;border:1px solid rgba(255,255,255,.8);border-radius:999em;padding:0 10px 0 10px;color:#fff;line-height:24px;font-size:12px;text-decoration:none;margin:0 1px;margin-bottom:6px;cursor:pointer}.tags a>sup,.tags .tag>sup{margin-left:-2px;font-weight:700}.tags a:hover,.tags .tag:hover,.tags a:active,.tags .tag:active{color:#fff;border-color:#fff;background-color:rgba(255,255,255,.4);text-decoration:none}@media only screen and (min-width:768px){.tags a,.tags .tag{margin-right:5px}}#tag-heading{padding:70px 0 60px}@media only screen and (min-width:768px){#tag-heading{padding:55px 0}}#tag_cloud{margin:20px 0 15px 0}#tag_cloud a,#tag_cloud .tag{transition-property:all;transition-duration:.4s;transition-timing-function:ease;font-size:14px;border:none;line-height:28px;margin:0 2px;margin-bottom:8px;background:#f3f5f5}#tag_cloud a:hover,#tag_cloud .tag:hover,#tag_cloud a:active,#tag_cloud .tag:active,#tag_cloud a.focus,#tag_cloud .tag.focus{background-color:#0085a1!important}#tag_cloud a.focus,#tag_cloud .tag.focus{box-shadow:rgba(0,0,0,.117647) 0 1px 6px,rgba(0,0,0,.239216) 0 1px 4px}#tag_cloud a.tag-button--all,#tag_cloud .tag.tag-button--all{font-weight:700;color:#0085a1!important}#tag_cloud a.tag-button--all:hover,#tag_cloud .tag.tag-button--all:hover,#tag_cloud a.tag-button--all:active,#tag_cloud .tag.tag-button--all:active,#tag_cloud a.tag-button--all.focus,#tag_cloud .tag.tag-button--all.focus{background-color:#e4e4e4!important}@media only screen and (min-width:768px){#tag_cloud{margin-bottom:25px}}.tag-comments{font-size:12px}@media only screen and (min-width:768px){.tag-comments{font-size:14px}}.t:first-child{margin-top:0}.listing-seperator{color:#0085a1;font-size:21px!important}.listing-seperator::before{margin-right:5px}@media only screen and (min-width:768px){.listing-seperator{font-size:20px!important;line-height:2!important}}.mini-post-list{margin:20px 0 15px 0}.mini-post-list .tag-text{font-weight:200;font-family:-apple-system,BlinkMacSystemFont,"Helvetica Neue",Arial,"PingFang SC","Hiragino Sans GB",STHeiti,"Microsoft YaHei","Microsoft JhengHei","Source Han Sans SC","Noto Sans CJK SC","Source Han Sans CN","Noto Sans SC","Source Han Sans TC","Noto Sans CJK TC","WenQuanYi Micro Hei",SimSun,sans-serif;line-height:1.7}.mini-post-list .post-preview{position:relative}.mini-post-list .post-preview>a .post-title{font-size:16px;font-weight:500;margin-top:20px}.mini-post-list .post-preview>a .post-subtitle{font-size:13px}.mini-post-list .post-preview>.post-meta{position:absolute;right:5px;bottom:0;margin:0;font-size:12px;line-height:12px}@media only screen and (min-width:768px){.mini-post-list .post-preview{margin-left:20px}.mini-post-list .post-preview>a>.post-title{font-size:18px;line-height:1.3}.mini-post-list .post-preview>a>.post-subtitle{font-size:14px}.mini-post-list .post-preview .post-meta{font-size:18px}}.post-container img{display:block;max-width:100%;height:auto;margin:1.5em auto 1.6em auto}.navbar-default .navbar-toggle:focus,.navbar-default .navbar-toggle:hover{background-color:inherit}.navbar-default .navbar-toggle:active{background-color:rgba(255,255,255,.25)}.navbar-default .navbar-toggle{border-color:transparent;padding:19px 16px;margin-top:2px;margin-right:2px;margin-bottom:2px;border-radius:50%}.navbar-default .navbar-toggle .icon-bar{width:18px;border-radius:0;background-color:#fff}.navbar-default .navbar-toggle .icon-bar+.icon-bar{margin-top:3px}.comment{margin-top:20px}.comment #ds-thread #ds-reset a.ds-like-thread-button{border:1px solid #ddd;border-radius:0;background:#fff;box-shadow:none;text-shadow:none}.comment #ds-thread #ds-reset li.ds-tab a.ds-current{border:1px solid #ddd;border-radius:0;background:#fff;box-shadow:none;text-shadow:none}.comment #ds-thread #ds-reset .ds-textarea-wrapper{background:0 0}.comment #ds-thread #ds-reset .ds-gradient-bg{background:0 0}.comment #ds-thread #ds-reset .ds-post-options{border-bottom:1px solid #ccc}.comment #ds-thread #ds-reset .ds-post-button{border-bottom:1px solid #ccc}.comment #ds-thread #ds-reset .ds-post-button{background:#fff;box-shadow:none}.comment #ds-thread #ds-reset .ds-post-button:hover{background:#eee}#ds-smilies-tooltip ul.ds-smilies-tabs li a{background:#fff!important}.page-fullscreen .intro-header{position:fixed;left:0;top:0;width:100%;height:100%}.page-fullscreen #tag-heading{position:fixed;left:0;top:0;padding-bottom:150px;width:100%;height:100%;display:-webkit-box;-webkit-box-orient:vertical;-webkit-box-pack:center;-webkit-box-align:center;display:-webkit-flex;-webkit-align-items:center;-webkit-justify-content:center;-webkit-flex-direction:column;display:flex;align-items:center;justify-content:center;flex-direction:column}.page-fullscreen footer{position:absolute;width:100%;bottom:0;padding-bottom:20px;opacity:.6;color:#fff}.page-fullscreen footer .copyright{color:#fff}.page-fullscreen footer .copyright a{color:#fff}.page-fullscreen footer .copyright a:hover{color:#ddd}.MathJax_SVG_Display{overflow:auto;-webkit-overflow-scrolling:touch}
\ No newline at end of file
diff --git a/less/hux-blog.less b/less/hux-blog.less
index 156e76b56f1..31a5e51bb63 100644
--- a/less/hux-blog.less
+++ b/less/hux-blog.less
@@ -178,7 +178,7 @@ samp {
     margin-bottom: 30px;
   }
   h4 {
-    font-size: 19px;
+    font-size: 22px;
     font-weight: 600;
     color: gray;
     & + p {
@@ -186,7 +186,7 @@ samp {
     }
   }
   h5, h6 {
-    font-size: 17px;
+    font-size: 20px;
     font-weight: 600;
     color: gray;
     & + p {
@@ -197,8 +197,9 @@ samp {
   @media screen and (max-width: 768px) {
     h1 { font-size: 30px; }
     h2 { font-size: 22px; }
-    h3 { font-size: 19px; }
-    h4 { font-size: 18px; }
+    h3 { font-size: 20px; }
+    h4 { font-size: 19px; }
+    h5, h6 { font-size: 18px; }
   }
   ul,
   ol {