search

isovector / haskell-language-server

Integration point for ghcide and haskell-ide-engine. One IDE to rule them all.
Apache License 2.0
0 stars 2 forks source link

Tactic tracing #26

Closed isovector closed 3 years ago

isovector commented 3 years ago

This PR implements tactic tracing; eg for foldr it produces this trace:

auto
`- intros {f_b, b, l_a}
   `- destruct(auto)
      `- destruct l_a
         +- match [] {}
         |  `- assume b
         `- match : {a, l_a4}
            `- apply' f_b
               +- assume a
               `- recursion
                  `- apply' myfoldr
                     +- assume f_b
                     +- assume b
                     `- assume l_a4

Fixes #25