diff --git a/src/ConETypeErase.ml b/src/ConETypeErase.ml
index b7903199..1bf55196 100644
--- a/src/ConETypeErase.ml
+++ b/src/ConETypeErase.ml
@@ -27,7 +27,7 @@ let rec tr_expr (e : S.expr) =
   match e with
   | EUnitPrf | EBoolPrf | EOptionPrf -> assert false
 
-  | ENum _ | ENum64 _ | EStr _ | EChr _ | EVar _ | EExtern _ ->
+  | ELit _ | EVar _ | EExtern _ ->
     let^ v = tr_expr_v e in
     T.EValue v
 
@@ -77,11 +77,7 @@ let rec tr_expr (e : S.expr) =
 and tr_expr_v (e : S.expr) =
   match e with
   | EUnitPrf | EBoolPrf | EOptionPrf -> assert false
-
-  | ENum   n        -> return (T.VLit (LNum n))
-  | ENum64 n        -> return (T.VLit (LNum64 n))
-  | EStr   s        -> return (T.VLit (LStr s))
-  | EChr   c        -> return (T.VLit (LNum (Char.code c)))
+  | ELit   l        -> tr_expr_lit l
   | EVar   x        -> return (T.VVar x)
 
   | EExtern(name, _) -> return (T.VExtern name)
@@ -105,6 +101,14 @@ and tr_expr_vs es =
     let* vs = tr_expr_vs es in
     return (v :: vs)
 
+(** Translate a literal *)
+and tr_expr_lit (l : S.literal) =
+  match l with
+  | ENum   n      -> return (T.VLit (LNum n))
+  | ENum64 n      -> return (T.VLit (LNum64 n))
+  | EStr   s      -> return (T.VLit (LStr s))
+  | EChr   c      -> return (T.VLit (LNum (Char.code c)))
+
 (** Translate a recursive definition *)
 and tr_rec_def (rd : S.rec_def) =
   (rd.rd_var, tr_expr rd.rd_body)
diff --git a/src/DblParser/Attributes.ml b/src/DblParser/Attributes.ml
index a66fe241..f550ee7f 100644
--- a/src/DblParser/Attributes.ml
+++ b/src/DblParser/Attributes.ml
@@ -35,6 +35,7 @@ type attr_conf = {
 let rec make_vis_pattern (pt : Lang.Surface.pattern) =
   map_node begin function
   | PWildcard -> PWildcard
+  | PLit l -> PLit l
   | PId (_, ident) -> PId (true, ident)
   | PAnnot (pt, scheme) -> PAnnot (make_vis_pattern pt, scheme)
   | PCtor (pth, xs, ys) -> 
diff --git a/src/DblParser/Desugar.ml b/src/DblParser/Desugar.ml
index a3f987aa..c007696d 100644
--- a/src/DblParser/Desugar.ml
+++ b/src/DblParser/Desugar.ml
@@ -307,10 +307,10 @@ let rec tr_pattern (p : Raw.expr) =
   | EWildcard   -> make PWildcard
   | EUnit | ECtor _ | ESelect _ ->
     make (PCtor(tr_ctor_pattern p, [], []))
-  | ENum _      -> Error.fatal (Error.desugar_error p.pos)
-  | ENum64 _      -> Error.fatal (Error.desugar_error p.pos)
-  | EStr _      -> Error.fatal (Error.desugar_error p.pos)
-  | EChr _      -> Error.fatal (Error.desugar_error p.pos)
+  | ENum      n -> make (PLit (ENum n))
+  | ENum64    n -> make (PLit (ENum64 n))
+  | EStr      s -> make (PLit (EStr s))
+  | EChr      c -> make (PLit (EChr c))
   | EInterp _   -> Error.fatal (Error.desugar_error p.pos)
   | EParen    p -> make (tr_pattern p).data
   | EVar      x -> make (PId(false, IdVar x))
@@ -546,10 +546,10 @@ and tr_expr (e : Raw.expr) =
   | EParen e       -> make (tr_expr e).data
   | EUnit | EVar _ | EImplicit _ | ECtor _ | EMethod _ | EBOpID _ | EUOpID _ ->
     make (EPoly(tr_poly_expr e, []))
-  | ENum n -> make (ENum n)
-  | ENum64 n -> make (ENum64 n)
-  | EStr s -> make (EStr s)
-  | EChr c -> make (EChr c)
+  | ENum n -> make (ELit(ENum n))
+  | ENum64 n -> make (ELit(ENum64 n))
+  | EStr s -> make (ELit(EStr s))
+  | EChr c -> make (ELit(EChr c))
   | EInterp (s, xs) ->
     let tr_toString (expr : Raw.expr) (fmt : Raw.expr option) = 
       let mth = { pos = expr.pos; data = (Raw.EMethod (expr, "toString"))} in
diff --git a/src/DblParser/Import.ml b/src/DblParser/Import.ml
index 3bfb3e6a..8764f87d 100644
--- a/src/DblParser/Import.ml
+++ b/src/DblParser/Import.ml
@@ -154,7 +154,7 @@ let define_module_path path =
   let open Lang.Surface in
   let make data = { pos = Position.nowhere; data } in
   make (DLetId(false, IdImplicit "~__modulePath__",
-    make (PE_Expr (make (EStr path)))))
+    make (PE_Expr (make (ELit(EStr path))))))
 
 let import_many imported imports =
   let mk_mod_def (n, imports, (d : File.def_list)) =
diff --git a/src/EffectInference/Expr.ml b/src/EffectInference/Expr.ml
index c0caa55f..ccf9429e 100644
--- a/src/EffectInference/Expr.ml
+++ b/src/EffectInference/Expr.ml
@@ -313,21 +313,24 @@ and infer_type : type ed.
       T.Type.subst sub sch.sch_body,
       return_pure eff_req )
 
-  | ENum n ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_int) in
-    (T.ENum n, tp, return_pure eff_req)
-
-  | ENum64 n ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_int64) in
-    (T.ENum64 n, tp, return_pure eff_req)
-
-  | EStr s ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_string) in
-    (T.EStr s, tp, return_pure eff_req)
-
-  | EChr c ->
-    let tp = T.Type.t_var (T.BuiltinType.tv_char) in
-    (T.EChr c, tp, return_pure eff_req)
+  | ELit l -> 
+    begin match l with
+    | ENum n ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_int) in
+      (T.ELit(ENum n), tp, return_pure eff_req)
+
+    | ENum64 n ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_int64) in
+      (T.ELit(ENum64 n), tp, return_pure eff_req)
+
+    | EStr s ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_string) in
+      (T.ELit(EStr s), tp, return_pure eff_req)
+
+    | EChr c ->
+      let tp = T.Type.t_var (T.BuiltinType.tv_char) in
+      (T.ELit(EChr c), tp, return_pure eff_req)
+    end
 
   | EFn(x, sch, body, _) ->
     let sch = Type.tr_scheme_expr env sch in
diff --git a/src/EffectInference/ExprUtils.ml b/src/EffectInference/ExprUtils.ml
index 8fe12cb7..281b6198 100644
--- a/src/EffectInference/ExprUtils.ml
+++ b/src/EffectInference/ExprUtils.ml
@@ -144,8 +144,7 @@ let mk_rec_ctx ~evs ~cs ~targs ~named all_defs =
 
 let rec update_rec_body ~rec_ctx (e : T.expr) : T.expr =
   match e with
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EExtern _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EExtern _ ->
     e
   
   | EVar x ->
diff --git a/src/EffectInference/Pattern.ml b/src/EffectInference/Pattern.ml
index 07784369..e5c9d926 100644
--- a/src/EffectInference/Pattern.ml
+++ b/src/EffectInference/Pattern.ml
@@ -76,6 +76,7 @@ end
 type t =
   | PWildcard
   | PAs       of t * T.var
+  | PLit      of T.literal 
   | PCtor     of
       { name  : string;
         idx   : int;
@@ -105,7 +106,7 @@ let open_tvars env targs tvars =
 
 let rec check_type env (pat : S.pattern) tp =
   match pat.data with
-  | PWildcard | PAnnot _ | POr _ ->
+  | PWildcard | PLit _ | PAnnot _ | POr _ ->
     check_scheme env pat (T.Scheme.of_type tp)
 
   | PAs(pat, x) ->
@@ -186,7 +187,36 @@ and check_scheme env (pat : S.pattern) sch =
   match pat.data with
   | PWildcard -> (PWildcard, PEnv.empty)
 
-  | PAs(pat, x) ->
+  | PLit l ->
+    let check_lit_scheme lit_tp =
+      begin match T.Scheme.to_type sch with
+      | Some tp ->
+          begin match T.Type.view tp, T.Type.view lit_tp with
+          | TVar x, TVar y -> assert (T.TVar.equal x y)
+          | _, _ -> assert false
+          end
+      | None -> assert false
+      end
+    in
+    begin match l with
+    | ENum n ->
+        check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int);
+        (PLit (ENum n), PEnv.empty)
+
+    | ENum64 n ->
+        check_lit_scheme (T.Type.t_var T.BuiltinType.tv_int64);
+        (PLit (ENum64 n), PEnv.empty)
+
+    | EStr s ->
+        check_lit_scheme (T.Type.t_var T.BuiltinType.tv_string);
+        (PLit (EStr s), PEnv.empty)
+
+    | EChr c ->
+        check_lit_scheme (T.Type.t_var T.BuiltinType.tv_char);
+        (PLit (EChr c), PEnv.empty)
+    end
+
+  | PAs(pat, x) -> 
     let (pat, penv) = check_scheme env pat sch in
     (PAs(pat, x), PEnv.add_var penv x sch)
 
diff --git a/src/EffectInference/Pattern.mli b/src/EffectInference/Pattern.mli
index 5a9540e4..804c7951 100644
--- a/src/EffectInference/Pattern.mli
+++ b/src/EffectInference/Pattern.mli
@@ -34,6 +34,7 @@ end
 type t =
   | PWildcard
   | PAs       of t * T.var
+  | PLit      of T.literal 
   | PCtor     of
       { name  : string;
         idx   : int;
diff --git a/src/EffectInference/PatternMatch.ml b/src/EffectInference/PatternMatch.ml
index 51e4692a..6a0eed1f 100644
--- a/src/EffectInference/PatternMatch.ml
+++ b/src/EffectInference/PatternMatch.ml
@@ -88,7 +88,8 @@ let drop_wildcard (cl : iclause) =
 let rec simplify_head x (cl : iclause) =
   match cl.c_patterns with
   | [] -> assert false
-  | PAs(pat, y) :: pats ->
+  | (PWildcard | PLit _ | PCtor _) :: pats   -> cl
+  | PAs(pat, y) :: pats -> 
     let cl =
       { cl with
         c_patterns = pat :: pats;
@@ -119,6 +120,8 @@ let simplify_ctor idx (ctor : T.ctor_decl) tvs cl =
     let pats2 = List.map (fun _ -> Pattern.PWildcard) ctor.ctor_arg_schemes in
     Some { cl with c_patterns = pats1 @ pats2 @ pats }
 
+  | PLit _ :: _  -> assert false
+
   | PCtor pc :: pats when pc.idx = idx ->
     assert (List.length pc.tvars = List.length tvs);
     assert (List.length pc.named = List.length ctor.ctor_named);
@@ -146,6 +149,10 @@ type column_class =
   | CC_Wildcard
     (** All patterns wild-cards *)
 
+  | CC_Lit of T.literal list
+    (** There is a literal pattern in the column. It stores the list of all
+      literals. *)
+
   | CC_ADT of T.expr * T.ctor_decl list
     (** There is a constructor pattern in the column. It stores computationally
       irrelevant proof of the shape of the constructor and the list of all
@@ -160,6 +167,21 @@ let rec column_class (cls : iclause list) =
     begin match cl.c_patterns with
     | [] -> assert false
     | PWildcard :: _ -> column_class cls
+    | PLit lit :: _ -> 
+        let rec collect acc cls = 
+          match cls with
+          | [] -> acc
+          | cl :: cls ->
+            (match cl.c_patterns with
+            | [] -> assert false
+            | PWildcard :: _ -> collect acc cls
+            | PLit l :: _ ->
+                if List.exists (fun x -> x = l) acc
+                then collect acc cls
+                else collect (l :: acc) cls
+            | (PCtor _ | PAs (_, _)) :: _ -> assert false)
+        in
+        CC_Lit (collect [lit] cls)
     | PCtor cp :: _ -> CC_ADT(cp.proof, cp.ctors)
     | PAs _ :: _ | POr _ :: _ ->
       (* As-patterns and or-patterns should be already simplified *)
@@ -193,16 +215,99 @@ module Make(Ctx : MatchContext) = struct
       cl.c_used := true;
       make_body cl
 
+<<<<<<< HEAD
+<<<<<<< HEAD
     | x :: xs, cls ->
       let cls = normalize_head_patterns x cls in
+=======
+    | x :: xs, cls ->    
+=======
+    | x :: xs, cls ->
+>>>>>>> ae0f7b7 (added requested changes)
+      let cls = simplify_as_patterns x cls in
+>>>>>>> c868a1f (Added pattern matching for literals)
       begin match column_class cls with
       | CC_Wildcard ->
         tr_match (refocus ctx) xs (List.map drop_wildcard cls)
 
+      | CC_Lit(lits) ->
+        tr_match_lit ctx x xs cls lits
+
       | CC_ADT(proof, ctors) ->
         let match_cls = List.mapi (tr_match_clause ctx xs cls) ctors in
         T.EMatch(proof, T.EVar x, match_cls, Ctx.res_tp, Ctx.res_eff)
       end
+  
+  and make_eq_type (lit: T.literal) = 
+    let tp_lit = 
+      match lit with 
+      | ENum n   -> T.Type.t_var T.BuiltinType.tv_int
+      | ENum64 n -> T.Type.t_var T.BuiltinType.tv_int64
+      | EStr s   -> T.Type.t_var T.BuiltinType.tv_string
+      | EChr c   -> T.Type.t_var T.BuiltinType.tv_char
+    in 
+    let tp_bool = T.Type.t_var T.BuiltinType.tv_bool in
+    let sch_lit = T.Scheme.of_type tp_lit in
+    let inner = T.Type.t_arrow sch_lit tp_bool T.Pure
+    in
+    T.Type.t_arrow sch_lit inner T.Pure
+
+  and make_eq_expr (x : T.expr) (lit : T.literal) : T.expr =
+    let eq_tp = make_eq_type lit in
+    match lit with
+    | ENum n ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.ELit(ENum n))
+    | ENum64 n ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt64", eq_tp), x), T.ELit(ENum64 n))
+    | EStr s ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqStr", eq_tp), x), T.ELit(EStr s))
+    | EChr c ->
+      T.EApp(T.EApp(T.EExtern("dbl_eqInt", eq_tp), x), T.ELit(EChr c))
+
+  and make_eq_match x lit then_e else_e =
+    let cond = make_eq_expr(T.EVar x) lit in
+    let cl_true =
+      { T.cl_tvars = [];
+        T.cl_vars  = [];
+        T.cl_body  = then_e 
+      } in
+    let cl_false =
+      { T.cl_tvars = [];
+        T.cl_vars  = [];
+        T.cl_body  = else_e 
+      } in
+    T.EMatch(T.EBoolPrf, cond, [cl_false; cl_true], Ctx.res_tp, Ctx.res_eff)
+
+  (** Build a match clause for a literal *)
+  and tr_match_lit ctx x xs cls lits =
+    let is_default cl = 
+      match cl.c_patterns with
+      | (PWildcard | PAs _)  :: _ -> true
+      | _ -> false 
+    in
+    let drop cl =
+      match cl.c_patterns with
+      | _ :: pats -> { cl with c_patterns = pats }
+      | [] -> assert false
+    in
+    let default_cls = List.filter is_default cls in
+    let default_branch =
+      match default_cls with
+      | [] -> Error.fatal (Error.non_exhaustive_match ~pos:Ctx.pos ctx)
+      | _ -> tr_match (refocus ctx) xs (List.map drop default_cls)
+    in
+    List.fold_right (fun lit acc ->
+      let cls_lit =
+      List.filter (fun cl ->
+        match cl.c_patterns with
+        | PLit l :: _ -> (l = lit)
+        | PWildcard :: _ -> true
+        | _ -> false)
+      cls
+    in
+    let branch = tr_match (refocus ctx) xs (List.map drop cls_lit) in
+    make_eq_match x lit branch acc)
+    lits default_branch
 
   (** Build a match clause for a single constructor. *)
   and tr_match_clause ctx xs cls idx (ctor : T.ctor_decl) =
diff --git a/src/Lang/ConE.mli b/src/Lang/ConE.mli
index ad561eb8..756318c4 100644
--- a/src/Lang/ConE.mli
+++ b/src/Lang/ConE.mli
@@ -127,17 +127,8 @@ type expr =
   | EOptionPrf
     (** ADT-shape proof for option type *)
 
-  | ENum of int
-    (** Integer literal *)
-
-  | ENum64 of int64
-    (** 64 bit integer literal *)
-
-  | EStr of string
-    (** String literal *)
-
-  | EChr of char
-    (** Character literal *)
+  | ELit of literal
+    (** Literal *)
 
   | EVar of var
     (** Variable *)
@@ -239,6 +230,13 @@ and match_clause =
     (** Body of the clause *)
   }
 
+(** Literals for patterns *)
+and literal =
+  | ENum        of int
+  | ENum64      of int64
+  | EStr        of string
+  | EChr        of char
+
 (** Programs *)
 type program = expr
 
diff --git a/src/Lang/ConEPriv/SExprPrinter.ml b/src/Lang/ConEPriv/SExprPrinter.ml
index 43fd8254..61fe3ec7 100644
--- a/src/Lang/ConEPriv/SExprPrinter.ml
+++ b/src/Lang/ConEPriv/SExprPrinter.ml
@@ -105,10 +105,7 @@ let rec tr_expr (e : expr) =
   | EUnitPrf   -> Sym "unit-prf"
   | EBoolPrf   -> Sym "bool-prf"
   | EOptionPrf -> Sym "option-prf"
-  | ENum n     -> Sym (string_of_int n)
-  | ENum64 n   -> Sym (Int64.to_string n ^ "L")
-  | EStr s     -> Sym (Printf.sprintf "\"%s\"" (String.escaped s))
-  | EChr c     -> Sym (Printf.sprintf "\'%s\'" (Char.escaped c))
+  | ELit l     -> tr_lit l
   | EVar x     -> tr_var x
   | EFn _      -> List (Sym "fn" :: tr_fn e)
   | ETFun _    -> List (Sym "tfun" :: tr_tfun e)
@@ -141,6 +138,13 @@ let rec tr_expr (e : expr) =
   | EReplExpr(e1, tp, e2) ->
     List [ Sym "repl-expr"; tr_expr e1; Sym ("{" ^ tp ^ "}"); tr_expr e2 ]
 
+and tr_lit l = 
+  match l with 
+  | ENum n     -> Sym (string_of_int n)
+  | ENum64 n   -> Sym (Int64.to_string n ^ "L")
+  | EStr s     -> Sym (Printf.sprintf "\"%s\"" (String.escaped s))
+  | EChr c     -> Sym (Printf.sprintf "\'%s\'" (Char.escaped c))
+
 and tr_fn e =
   match e with
   | EFn(x, sch, e) ->
@@ -158,10 +162,9 @@ and tr_app e args =
   | ETApp(e1, tp) -> tr_app e1 (List [ Sym "type"; tr_type tp ] :: args)
   | ECApp e1 -> tr_app e1 (Sym "constr" :: args)
 
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EVar _ | EFn _ | ETFun _ | ECAbs _ | ELet _ | ELetPure _ | ELetRec _ 
-  | ERecCtx _ | EData _ | ECtor _ | EMatch _ | EShift _ | EReset _ | EExtern _
-  | ERepl _ | EReplExpr _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _
+  | ECAbs _ | ELet _ | ELetPure _ | ELetRec _ | ERecCtx _ | EData _ | ECtor _
+  | EMatch _ | EShift _ | EReset _ | EExtern _ | ERepl _ | EReplExpr _ ->
     List (tr_expr e :: args)
 
 and tr_defs e =
@@ -182,9 +185,9 @@ and tr_defs e =
         tr_var x; tr_expr ret
       ] :: tr_defs body
 
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EVar _ | EFn _ | ETFun _ | ECAbs _ | EApp _ | ETApp _ | ECApp _ | ECtor _
-  | EMatch _ | EShift _ | EExtern _ | ERepl _ | EReplExpr _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _
+  | ECAbs _ | EApp _ | ETApp _ | ECApp _ | ECtor _ | EMatch _ | EShift _
+  | EExtern _ | ERepl _ | EReplExpr _ ->
     [ tr_expr e ]
 
 and tr_rec_def rd =
diff --git a/src/Lang/ConEPriv/Syntax.ml b/src/Lang/ConEPriv/Syntax.ml
index 227de25b..c6054ff1 100644
--- a/src/Lang/ConEPriv/Syntax.ml
+++ b/src/Lang/ConEPriv/Syntax.ml
@@ -27,10 +27,7 @@ type expr =
   | EUnitPrf
   | EBoolPrf
   | EOptionPrf
-  | ENum      of int
-  | ENum64    of int64
-  | EStr      of string
-  | EChr      of char
+  | ELit      of literal
   | EVar      of var
   | EFn       of var * scheme * expr
   | ETFun     of tvar * expr
@@ -50,6 +47,11 @@ type expr =
   | EExtern   of string * typ
   | ERepl     of (unit -> expr) * typ * ceffect
   | EReplExpr of expr * string * expr
+and literal =
+  | ENum      of int
+  | ENum64    of int64
+  | EStr      of string
+  | EChr      of char
 
 and rec_def =
   { rd_var    : var;
diff --git a/src/Lang/Surface.ml b/src/Lang/Surface.ml
index a6e38b97..2ba5882d 100644
--- a/src/Lang/Surface.ml
+++ b/src/Lang/Surface.ml
@@ -172,11 +172,27 @@ and ctor_decl_data = {
   cd_arg_schemes : scheme_expr list
 }
 
+(** Literals *)
+type literal =
+  | ENum of int
+    (** Integer literal *)
+
+  | ENum64 of int64
+    (** 64 bit integer literal *)
+
+  | EStr of string
+    (** String literal *)
+
+  | EChr of char
+    (** Char literal *)
+
 (** Patterns *)
 type pattern = pattern_data node
 and pattern_data =
   | PWildcard
     (** Wildcard pattern -- it matches everything *)
+  
+  | PLit of literal
 
   | PId of is_public * ident
     (** Pattern that binds an identifier *)
@@ -240,17 +256,8 @@ and expr_data =
     (** Unit expression. Used only as the expression after the last definition
       in a program. *)
 
-  | ENum of int
-    (** Integer literal *)
-
-  | ENum64 of int64
-    (** 64 bit integer literal *)
-
-  | EStr of string
-    (** String literal *)
-
-  | EChr of char
-    (** Char literal *)
+  | ELit of literal
+    (** Literal *)
 
   | EPoly of poly_expr_use * inst list
     (** Polymorphic expression with partial explicit instantiation, possibly
diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli
index a4ce5d5b..a8556d7c 100644
--- a/src/Lang/Unif.mli
+++ b/src/Lang/Unif.mli
@@ -277,6 +277,20 @@ type proof_expr =
     (** Variable generated at the ADT definition, applied to the parameters
       of the ADT. *)
 
+(* Literal *)
+type literal =
+  | ENum of int
+    (** Integer literal *)
+
+  | ENum64 of int64
+    (** 64 bit integer literal *)
+
+  | EStr of string
+    (** String literal *)
+
+  | EChr of char
+    (** Character literal *)
+
 (** Pattern *)
 type pattern = pattern_data node
 and pattern_data =
@@ -286,6 +300,9 @@ and pattern_data =
   | PAs of pattern * var
     (** Pattern that binds a variable and continues with a subpattern *)
 
+  | PLit of literal 
+    (** Literal pattern *)
+
   | PCtor of
     string * int * proof_expr * tvar list * pattern list * pattern list
     (** ADT constructor pattern. It stores a name, constructor index,
@@ -298,6 +315,12 @@ and pattern_data =
   | POr of pattern * pattern
     (** Or-pattern: matches if either sub-pattern matches *)
 
+and literal =   
+  | PNum of int
+  | PNum64 of int64
+  | PStr of string
+  | PChr of char
+
 (** Polymorphic expression *)
 type poly_expr = poly_expr_data node
 and poly_expr_data =
@@ -335,17 +358,8 @@ and expr_data =
   | EInst of poly_expr * type_expr list * poly_fun list
     (** Instantiation of polymorphic expression *)
 
-  | ENum of int
-    (** Integer literal *)
-
-  | ENum64 of int64
-    (** 64 bit integer literal *)
-
-  | EStr of string
-    (** String literal *)
-
-  | EChr of char
-    (** Character literal *)
+  | ELit of literal
+    (* Literal *)
 
   | EFn of var * scheme_expr * expr * effct
     (** Effect-annotated lambda-abstraction. *)
diff --git a/src/Lang/UnifPriv/Ren.ml b/src/Lang/UnifPriv/Ren.ml
index 2f43fa98..41d53be3 100644
--- a/src/Lang/UnifPriv/Ren.ml
+++ b/src/Lang/UnifPriv/Ren.ml
@@ -71,6 +71,7 @@ let rec rename_pattern ren (pat : pattern) =
     match pat.data with
     | PWildcard   -> PWildcard
     | PAs(pat, x) -> PAs(rename_pattern ren pat, rename_var ren x)
+    | PLit(lit)   -> PLit(lit)
     | PCtor(name, idx, prf, tvars, pats1, pats2) ->
       PCtor(name, idx, rename_proof_expr ren prf,
              List.map (rename_tvar ren) tvars,
diff --git a/src/Lang/UnifPriv/Syntax.ml b/src/Lang/UnifPriv/Syntax.ml
index b7bf4a27..0134b958 100644
--- a/src/Lang/UnifPriv/Syntax.ml
+++ b/src/Lang/UnifPriv/Syntax.ml
@@ -77,15 +77,28 @@ type proof_expr =
   | PE_Option of typ
   | PE_Var    of var * typ list
 
+type literal =
+  | ENum      of int
+  | ENum64    of int64
+  | EStr      of string
+  | EChr      of char
+
 type pattern = pattern_data node
 and pattern_data =
   | PWildcard
   | PAs       of pattern * var
+  | PLit      of literal
   | PCtor     of
     string * int * proof_expr * tvar list * pattern list * pattern list
   | PAnnot    of pattern * scheme_expr
   | POr       of pattern * pattern
 
+and literal =
+  | PNum      of int
+  | PNum64    of int64
+  | PStr      of string
+  | PChr      of char
+
 type poly_expr = poly_expr_data node
 and poly_expr_data =
   | EVar     of var
@@ -101,10 +114,7 @@ and poly_fun_data =
 and expr = expr_data node
 and expr_data =
   | EInst       of poly_expr * type_expr list * poly_fun list
-  | ENum        of int
-  | ENum64      of int64
-  | EStr        of string
-  | EChr        of char
+  | ELit        of literal
   | EFn         of var * scheme_expr * expr * effct
   | EAppPoly    of expr * poly_fun
   | EAppMono    of expr * expr
diff --git a/src/ToCore/Main.ml b/src/ToCore/Main.ml
index eb5b56d2..3a7ed9ac 100644
--- a/src/ToCore/Main.ml
+++ b/src/ToCore/Main.ml
@@ -14,8 +14,8 @@ let return x cont = cont x
 (** Translate expression *)
 let rec tr_expr env (e : S.expr) =
   match e with
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EVar _ | EExtern _ | ERepl _ | EReplExpr _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EExtern _ | ERepl _
+  | EReplExpr _ ->
     let^ v = tr_expr_v env e in
     T.EValue v
 
@@ -90,8 +90,8 @@ and tr_let_expr ~pure x env (e : S.expr) cont =
   | _ when pure ->
     T.ELetPure(Relevant, x, tr_expr env e, cont ())
 
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _ 
-  | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _
+  | ECAbs _ | EExtern _ ->
     T.ELetPure(Relevant, x, tr_expr env e, cont ())
 
   | EApp _ | ETApp _ | ECApp _ | ELet _ | ELetPure _ | ELetRec _ | ERecCtx _
@@ -116,8 +116,8 @@ and tr_expr_as_var env e =
 (** Translate an expression as pure expression *)
 and tr_expr_p env (e : S.expr) =
   match e with
-  | EUnitPrf | EBoolPrf | EOptionPrf | ENum _ | ENum64 _ | EStr _ | EChr _
-  | EVar _ | EFn _ | ETFun _ | ECAbs _ | EExtern _ ->
+  | EUnitPrf | EBoolPrf | EOptionPrf | ELit _ | EVar _ | EFn _ | ETFun _
+  | ECAbs _ | EExtern _ ->
     return (tr_expr env e)
 
   | ETApp(e, tp) ->
@@ -164,11 +164,7 @@ and tr_expr_v env (e : S.expr) =
   | EUnitPrf   -> return v_unit_prf
   | EBoolPrf   -> return v_bool_prf
   | EOptionPrf -> return v_option_prf
-
-  | ENum   n -> return (T.VLit (LNum n))
-  | ENum64 n -> return (T.VLit (LNum64 n))
-  | EStr   s -> return (T.VLit (LStr s))
-  | EChr   c -> return (T.VLit (LNum (Char.code c)))
+  | ELit   l -> tr_lit l
   | EVar   x -> return (T.VVar x)
 
   | ELet(x, e1, e2) ->
@@ -188,6 +184,14 @@ and tr_expr_v env (e : S.expr) =
     let* x = tr_expr_as_var env e in
     return (T.VVar x)
 
+(** Translate a literal *)
+and tr_lit l =
+  match l with 
+  | ENum   n -> return (T.VLit (LNum n))
+  | ENum64 n -> return (T.VLit (LNum64 n))
+  | EStr   s -> return (T.VLit (LStr s))
+  | EChr   c -> return (T.VLit (LNum (Char.code c)))
+
 (** Translate a list of expressions as list of values in expression building
   monad. *)
 and tr_expr_vs env es =
diff --git a/src/TypeInference/Expr.ml b/src/TypeInference/Expr.ml
index 243d1f89..8492655a 100644
--- a/src/TypeInference/Expr.ml
+++ b/src/TypeInference/Expr.ml
@@ -37,33 +37,33 @@ let infer_expr_type ~tcfix ?app_type env (e : S.expr) =
       er_constr = []
     }
 
-  | ENum n ->
-    { er_expr   = make (T.ENum n);
-      er_type   = Infered (T.Type.t_var T.BuiltinType.tv_int);
-      er_effect = Pure;
-      er_constr = []
-    }
-
-  | ENum64 n ->
-    { er_expr   = make (T.ENum64 n);
-      er_type   = Infered (T.Type.t_var T.BuiltinType.tv_int64);
-      er_effect = Pure;
-      er_constr = []
-    }
-
-  | EStr s ->
-    { er_expr   = make (T.EStr s);
-      er_type   = Infered (T.Type.t_var T.BuiltinType.tv_string);
-      er_effect = Pure;
-      er_constr = []
-    }
-
-  | EChr c ->
-    { er_expr   = make (T.EChr c);
+  | ELit l -> 
+    begin match l with
+    | ENum n ->
+      { er_expr   = make (T.ELit(ENum n));
+        er_type   = Infered (T.Type.t_var T.BuiltinType.tv_int);
+        er_effect = Pure;
+        er_constr = []
+      }
+    | ENum64 n ->
+      { er_expr   = make (T.ELit(ENum64 n));
+        er_type   = Infered (T.Type.t_var T.BuiltinType.tv_int64);
+        er_effect = Pure;
+        er_constr = []
+      }
+    | EStr s ->
+      { er_expr   = make (T.ELit(EStr s));
+        er_type   = Infered (T.Type.t_var T.BuiltinType.tv_string);
+        er_effect = Pure;
+        er_constr = []
+      }
+    | EChr c ->
+    { er_expr   = make (T.ELit(EChr c));
       er_type   = Infered (T.Type.t_var T.BuiltinType.tv_char);
       er_effect = Pure;
       er_constr = []
     }
+    end
 
   | EPoly(e, inst) ->
     let (p_ctx, e, sch) = PolyExpr.infer_use_scheme ~tcfix ?app_type env e in
@@ -316,7 +316,7 @@ let check_expr_type ~tcfix env (e : S.expr) tp =
   let pp = Env.pp_tree env in
   let make data = T.{ pos; pp; data } in
   match e.data with
-  | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EPoly _ | EApp _
+  | EUnit | ELit _ | EPoly _ | EApp _
   | EAnnot _ | EAnnotEff _ | EAnnotTotal _ ->
     check_expr_type_default ~tcfix env e tp
 
diff --git a/src/TypeInference/ParamResolve.ml b/src/TypeInference/ParamResolve.ml
index e7618a9f..fe4150b8 100644
--- a/src/TypeInference/ParamResolve.ml
+++ b/src/TypeInference/ParamResolve.ml
@@ -244,9 +244,9 @@ and resolve_implicit ~resolve_env rctx iname sch =
     (* Special implicits *)
     let (param_expr, param_tvar) = match iname with
       | "~__line__" -> 
-        (make (T.ENum pos.pos_start_line), T.BuiltinType.tv_int)
+        (make (T.ELit(ENum pos.pos_start_line)), T.BuiltinType.tv_int)
       | "~__file__" -> 
-        (make (T.EStr pos.pos_fname), T.BuiltinType.tv_string)
+        (make (T.ELit(EStr pos.pos_fname)), T.BuiltinType.tv_string)
       | _ -> Error.fatal (Error.cannot_resolve_implicit ~pos iname) in
     (* Check types *)
     let param_sch = T.Scheme.of_type (T.Type.t_var param_tvar) in
diff --git a/src/TypeInference/Pattern.ml b/src/TypeInference/Pattern.ml
index 94411b88..1dc7139d 100644
--- a/src/TypeInference/Pattern.ml
+++ b/src/TypeInference/Pattern.ml
@@ -193,6 +193,13 @@ let tr_named_scheme_annot env (name : Name.t) sch_expr =
 
 (* ========================================================================= *)
 
+let literal_type (lit : S.literal) =
+  match lit with
+  | ENum _   -> T.Type.t_var T.BuiltinType.tv_int
+  | ENum64 _ -> T.Type.t_var T.BuiltinType.tv_int64
+  | EStr _   -> T.Type.t_var T.BuiltinType.tv_string
+  | EChr _   -> T.Type.t_var T.BuiltinType.tv_char
+      
 let rec check_scheme env (pat : S.pattern) sch =
   let pos = pat.pos in
   let pp = Env.pp_tree env in
@@ -201,11 +208,28 @@ let rec check_scheme env (pat : S.pattern) sch =
   | PWildcard ->
     (PartialEnv.empty, make T.PWildcard, T.Pure)
 
-  | PId(public, id) ->
+  | PLit l ->
+    let lit_tp = literal_type l in
+    begin match T.Scheme.to_type sch with
+    | None ->
+        Error.fatal (Error.non_polymorphic_pattern ~pos)
+    | Some tp ->
+        Error.check_unify_result ~pos
+          (Unification.subtype env lit_tp tp)
+          ~on_error:(Error.pattern_type_mismatch ~pp lit_tp tp);
+    end; 
+    begin match l with
+    | ENum n   -> (PartialEnv.empty, make (T.PLit(T.ENum n)), T.Pure)
+    | ENum64 n -> (PartialEnv.empty, make (T.PLit(T.ENum64 n)), T.Pure)
+    | EStr s   -> (PartialEnv.empty, make (T.PLit(T.EStr s)), T.Pure)
+    | EChr c   -> (PartialEnv.empty, make (T.PLit(T.EChr c)), T.Pure)
+    end
+
+  | PId(public, id) -> 
     let name = NameUtils.tr_ident ~pos ~pp id sch in
     let x = Var.fresh ~name:(Name.to_string name) () in
     let penv = PartialEnv.singleton_val ~public ~pos name x sch in
-    (penv, make (T.PAs(make T.PWildcard, x)), T.Pure)
+    (penv, make (T.PAs(make T.PWildcard, x)), T.Pure) 
 
   | PCtor _ ->
     begin match T.Scheme.to_type sch with
@@ -241,7 +265,7 @@ and check_type env (pat : S.pattern) tp =
   let pp = Env.pp_tree env in
   let make data = T.{ pos; pp; data } in
   match pat.data with
-  | PWildcard | PId _ | PAnnot _ | POr _ ->
+  | PWildcard | PLit _ | PId _ | PAnnot _ | POr _ ->
     let sch = T.Scheme.of_type tp in
     check_scheme env pat sch
 
@@ -384,7 +408,11 @@ and check_named_pattern env np tvars named =
 
 let infer_scheme env (pat : S.pattern) =
   match pat.data with
+<<<<<<< HEAD
   | PWildcard | PId _ | PCtor _ | POr _ ->
+=======
+  | PWildcard | PLit _ | PId _ | PCtor _ ->
+>>>>>>> c868a1f (Added pattern matching for literals)
     let tp = Env.fresh_uvar ~pos:pat.pos env T.Kind.k_type in
     let tp_expr =
       { T.pos  = pat.pos;
diff --git a/src/TypeInference/RecDefs.ml b/src/TypeInference/RecDefs.ml
index 2e21e116..a6fefd7a 100644
--- a/src/TypeInference/RecDefs.ml
+++ b/src/TypeInference/RecDefs.ml
@@ -56,8 +56,9 @@ let rec prepare_rec_data env (def : S.def) =
     | PAnnot({ data = PId(public, id); _ }, sch) ->
       (env, make (D1_Label(x, public, id, Some(pat.pos, sch))))
 
-    | PAnnot({ data = PWildcard | PCtor _ | PAnnot _ | POr _; _ }, _)
-    | PWildcard | PCtor _ | POr _ ->
+    | PAnnot({ data = PWildcard | PLit _ | PCtor _ | PAnnot _ | POr _; _ }, _)
+
+    | PWildcard | PLit _ | PCtor _ | POr _ ->
       Error.fatal (Error.invalid_rec_def ~pos:def.pos)
     end
 
@@ -304,8 +305,8 @@ let rec guess_rec_fun_type env (e : S.expr) tp =
       rfb_body_tp = tp
     }, T.Impure
 
-  | EUnit | ENum _ | ENum64 _ | EStr _ | EChr _ | EPoly _ | EApp _ | EDefs _
-  | EMatch _ | EHandler _ | EHandlerFn _ | EEffect _ | EExtern _ | ERepl _ ->
+  | EUnit | ELit _ | EPoly _ | EApp _ | EDefs _ | EMatch _ | EHandler _
+  | EHandlerFn _ | EEffect _ | EExtern _ | ERepl _ ->
     let pp = Env.pp_tree env in
     { rfb_type    = { T.pos = pos; T.pp = pp; T.data = T.TE_Type tp };
       rfb_args    = [];
@@ -544,7 +545,7 @@ let update_rec_body ~pos fds (body : T.poly_fun) =
     let make data = { body with data = data } in
     match e.data with
 
-    | ENum _ | ENum64 _ | EStr _ | EChr _ | EExtern _ -> e
+    | ELit _ | EExtern _ -> e
 
     | EFn(x, sch, body, Impure) ->
       make (T.EFn(x, sch, make (T.ERecCtx body), Impure))
diff --git a/test/ok/ok0154_literalMatch.fram b/test/ok/ok0154_literalMatch.fram
new file mode 100644
index 00000000..e51b22cc
--- /dev/null
+++ b/test/ok/ok0154_literalMatch.fram
@@ -0,0 +1,37 @@
+let f (x: Int) =
+  match x with
+  | 0 => 0
+  | 1 => 1
+  | 2 => 2
+  | _ => 3
+  end
+
+let fs (s: String) = 
+  match s with
+  | "fram" => "fram"
+  | "compiler" => "not found :("
+  | _ => "abcd"
+  end
+
+let fc (c: Char) = 
+  match c with
+  | 'a' => 'a'
+  | 'b' => 'b'
+  | _ => 'c'
+  end
+
+data Pair X Y = (,) of X, Y
+
+let fp x y =
+  match (x,y) with
+  | (1,2) => 1
+  | (_,_) => 0
+  end
+
+let _ = f 3
+let _ = fs "abc"
+let _ = fc 'x'
+let _ = fp 1 2 
+
+
+