Ssreflect Users Discussion List

[Felipe Cerqueira <>]

Hi,

Today I was trying to instantiate concrete types in my specification to 
make sure the hypotheses are correct.
I was able to run 'Eval compute in ...' with simple list functions, but 
my specification is full of big operators.
I tried code extraction to Haskell and it seems to work fine.
But is it possible to test the computation inside Coq so that I could 
run small examples more easily?

Currently I get a very long output like this:

 if (fix all (s : seq (concrete_task * nat)) : bool :=
             match s with
             | [::] => true
             | x :: s' =>
                 if let (tsk, R) := x in
                    (fix eqn (m n : nat) {struct m} : bool :=
                       match m with
                       | 0 => match n with
                              | 0 => true
                              | _.+1 => false
                              end
                       | m'.+1 =>
                           match n with
                           | 0 => false
                           | n'.+1 => eqn m' n'
                           end
                       end)
                      ((fix minus (n m : nat) {struct n} : nat :=
                          match n with
                          | 0 => n
                          | k.+1 =>
                              match m with
                              | 0 => n
                              | l.+1 => minus k l
                              end
                          end) R
                         (let (_, _, task_deadline) := tsk in 
task_deadline))
           ...


Thanks,
Felipe