Andrew Johnson

**Is your feature request related to a problem? Please describe.** Schubert's Steamroller was an early auto proof. [A clear and concise description of what the problem is. Ex. I'm always...

**Is your feature request related to a problem? Please describe.** Rust has a nice new DFA library, we should use it. **Describe the solution you'd like** L1DFA has operations like...

FIXME

1

**Describe the bug** There is a lot of FIXME commented code in the test suite. **To Reproduce** grep "FIXME" tests/* **Expected behavior** No FIXMEs

Implement reverse operator for regular expressions

1

**Is your feature request related to a problem? Please describe.** It would be nice for CFG types to allow both left and right recursion. To support this, DFAs must be...

**Is your feature request related to a problem? Please describe.** Hints may need to be parameterized to prove a goal. This parameter should be a single term so that hints...

**Is your feature request related to a problem? Please describe.** LSTS should be a frontend for LM. **Describe the solution you'd like** LM should be a frontend for LM.

With typed fragments this Term case is no longer necessary.

Make c libraries callable

``` (: y Sized). ( x ) ``` needs an error to indicate that an ascripted type is expected ``` (: x L) ```

Now branch conditionals can handle Boolean values correctly.