Parsing `lfind_eval` output

[yalhessi]

There's a problem with parsing the output of lfind_eval when I run with CoqSynth. This doesn't exist when using myth because myth does extraction instead of parsing the output directly.

This can be replicated when run with even_list where it tries to evaluate Even so the value returned is actually a prop.

[yalhessi]

After looking more at the output here, here's one case that's handled correctly by the code we currently have:

     = Cons 4 (Cons 4 (Cons 4 (Cons 4 (Cons 4 Nil))))
     : lst
     = Cons 1 (Cons 1 (Cons 1 Nil))
     : lst
     = Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 (Cons 2 Nil)))))
     : lst
     = Cons 2 Nil
     : lst
     = Cons 3 (Cons 3 (Cons 3 (Cons 3 Nil)))
     : lst
     = Nil
     : lst
     = Nil
     : lst
     = Nil
     : lst
     = Cons 2 (Cons 2 Nil)
     : lst
     = Cons 6 Nil
     : lst
     = Cons 0 Nil
     : lst
     = Cons 0 (Cons 0 Nil)
     : lst
     = Cons 3 (Cons 3 Nil)
     : lst
     = Nil
     : lst
     = Cons 1 Nil
     : lst
     = Cons 4 (Cons 4 (Cons 4 Nil))
     : lst
     = Cons 4 (Cons 4 Nil)
     : lst
     = Nil
     : lst

Here's a different case that's not handled:

     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop
     = fun x : nat =>
       exists x0 : nat,
         x =
         (fix Ffix (x1 : nat) : nat :=
            match x1 with
            | 0 => 0
            | S x2 => S (S (Ffix x2))
            end) x0
     : nat -> Prop

From the second example, it's clear we need regex here to look forward when we're matching so to fix this we need to figure out how to include a regex library.