desugar match with implicit args

book/Equal/apply.kind2

@@ -1,10 +1,12 @@
-//use Equal/{refl}
-
 apply <A: *> <B: *> <a: A> <b: B> (f: A -> B) (e: (Equal A a b)) : (Equal B (f a) (f b)) =
   match e {
-    Equal/refl: {=}
-  }
+    Equal/refl: ~λPλrefl(refl (f e.a))
+  }: (Equal B (f a) (f b))
 
+  //(Equal/match
+    //λaλbλe(Equal B (f a) (f b))
+    //λx ~λPλrefl(refl (f x))
+    //e)
 
 //Equal.apply
 //: ∀(A: *)

book/Equal/match.kind2

@@ -0,0 +1,6 @@
+match <T: *> <a: T> <b: T> 
+  (P: ∀(a:T) ∀(b:T) ∀(e: (Equal T a b)) *)
+  (refl: ∀(x: T) (P x x (Equal/refl/ T x)))
+  (e: (Equal T a b))
+: (P a b e) =
+  (~e P refl)

src/sugar/mod.rs

@@ -919,17 +919,17 @@ impl Term {
       }
     }
 
-    // 3. Create `(Type/fold|match <param_holes> <motive>)`
+    // 3. Create `(Type/fold|match <motive>)`
     term = Term::Var {
-      nam: format!("{}/{}/", adt.name, if mat.fold { "fold" } else { "match" })
+      nam: format!("{}/{}", adt.name, if mat.fold { "fold" } else { "match" })
     };
-    for _par in &adt.pars {
-      term = Term::App {
-        era: true,
-        fun: Box::new(term),
-        arg: Box::new(Term::Met {}),
-      };
-    }
+    //for _par in &adt.pars {
+      //term = Term::App {
+        //era: true,
+        //fun: Box::new(term),
+        //arg: Box::new(Term::Met {}),
+      //};
+    //}
     term = Term::App {
       era: true,
       fun: Box::new(term),
@@ -995,6 +995,9 @@ impl Term {
       bod: Box::new(term)
     };
 
+    // Debug: Prints the generated term
+    //println!("{}", term.format().flatten(Some(800)));
+
     // 10. Return 'term'
     return term;
   }