improve leancheck to handle #def

src/leancheck/leancheck.ml

@@ -175,6 +175,14 @@ let process_files ~max_err ~quiet (files : string list) : unit =
           );
           ()
 
+        let def ~nidx ~tyidx ~validx ~univ_params : unit =
+          let name = Idx.get_name idx nidx in
+          let _ty = Lean_elab.elab_top (Idx.get_term idx tyidx) in
+          let _val = Lean_elab.elab_top (Idx.get_term idx validx) in
+          let _univ_params = List.map (Idx.get_name idx) univ_params in
+          if not quiet then
+            Fmt.eprintf "@[<2>@{<Blue>Def@}@ %s@]@." name
+
         let after_line () =
           if quiet then (
             if !n_lines mod 1000 = 0 then Fmt.eprintf "\rlines: %d%!" !n_lines

src/leancheck/parse.ml

@@ -100,6 +100,15 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
                l
            in
            CB.ind ~n_params ~nidx ~tyidx ~intros ~univ_params
+         | S "#DEF" :: I nidx :: I tyidx :: I validx :: tl ->
+           let univ_params =
+             List.map
+               (function
+                 | I i -> i
+                 | _ -> failwith "invalid param")
+               tl
+           in
+           CB.def ~nidx ~tyidx ~validx ~univ_params
          | _ ->
            incr n_errors;
            Fmt.eprintf "@{<Yellow>warn@}: unhandled line %d: %s@." !n_line line

src/leancheck/parse_intf.ml

@@ -21,4 +21,7 @@ module type CALLBACK = sig
     intros:(int * int) list ->
     univ_params:int list ->
     unit
+
+  val def :
+    nidx:int -> tyidx:int -> validx:int -> univ_params:int list -> unit
 end