Search results

[Usability] Four test cases in tests.ts have empty descriptions — failures are unidentifiable

Status: Open.

#186 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Usability] No replace tactic — transport along equality requires writing a full exact term

Status: Open.

#185 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Usability] No refl tactic — users must write exact (same ...) for reflexivity goals

Status: Open.

#184 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Usability] elim-Equal tactic always requires an explicit motive

Status: Open.

#183 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Usability] elim-Vec tactic requires explicit motive and length — should auto-generate like elim-Nat/elim-List

Status: Open.

#182 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Bug] Web editor diagnostics worker is a stub — no real-time error feedback, hover, or completions

bugSomething isn't workingSomething isn't working

Status: Open.

#181 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Bug] package.json main field points to a .ts source file instead of compiled .js

bugSomething isn't workingSomething isn't working

Status: Open.

#180 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Bug]: SpiltTactic computes wrong cdrType — second Sigma goal is incorrectly typed

bugSomething isn't workingSomething isn't working

Status: Open.

#179 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Bug]: return stop instead of return result in GeneralTypeConstructor.checkOut

bugSomething isn't workingSomething isn't working

Status: Open.

#178 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Bug]: AI TODO solver receives empty context

bugSomething isn't workingSomething isn't working

Status: Open.

#177 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 23, 2026

[Feature]: Implementing Proof History

Status: Open.

Feature

#176 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 22, 2026

[Bug]: Tactics UI error

bugSomething isn't workingSomething isn't working

Status: Open.

#175 In source-academy/pie-slang;

· MarcusMa06-code opened on Apr 22, 2026