PR !4#11142: feat(ProofTheory): Define logical symbols ab...

Stream: triage

[Random Issue Bot]

Today I chose PR #11142 for discussion!

feat(ProofTheory): Define logical symbols abstractly; opens new top-level section, drawing from lean4-logic
Created by @Hunter Monroe (@hmonroe) on 2024-03-04
Labels: awaiting-author, merge-conflict, t-logic

Is this PR still relevant? Any recent updates? Anyone making progress?