incorporate feedback from AE review

Author: yongweiy

README.md

@@ -2,7 +2,7 @@
 This repo includes artifacts for "Live Pattern Matching with Typed Holes". Specifically,
 
 - Folder `agda-mechanization` contains a proof mechanization that concludes the type safety of the system presented in the paper.
-- Folder `incon-sat` contains a minimal implementation of exhaustiveness and redundancy checking based on SAT solving (as described in Sec 4.7.1 of the paper). Instead of type checking a program with holes, it simply focuses on checking consistency between constraints ξ, which resemble patterns p. 
+- Folder `incon-sat` contains a minimal implementation of exhaustiveness and redundancy checking based on SAT solving (as described in Sec 4.7.1 of the paper). Instead of type checking a program with holes, it simply focuses on checking consistency between constraints ξ, which resemble patterns p. The integration into [Hazel](https://hazel.org/) can be found [here](https://github.com/hazelgrove/hazel/tree/adts-plus-match), which [implements](https://github.com/hazelgrove/hazel/blob/adts-plus-match/src/hazelcore/Incon.re) the algorithm described in Sec 4.7.2 and the extension with finite labeled sums described in Sec 5 .
 
 ## Kick The Tires
 
@@ -15,13 +15,19 @@ This repo includes artifacts for "Live Pattern Matching with Typed Holes". Speci
 
 - Build and run Agda mechanization
   ```
+  $ docker pull pattern-agda
   $ docker build -t pattern-agda agda-mechanization
   $ docker run pattern-agda # will check proof
   ```
 - Build and run Exhaustiveness and Redundancy Checker
   ```
-  $ docker build -t pattern-incon agda-mechanization
+  $ docker build -t pattern-incon incon-sat
   $ docker run -it pattern-incon # will invoke OCaml toplevel
   ``` 
+- Pre-built dockers are available.
+  ```
+  $ docker pull victoryuan/pattern-agda
+  $ docker pull victoryuan/pattern-incon
+  ```
 
 Please see the README in each folder for detailed instructions.