Skip to content

Commit daa2673

Browse files
First stable conversion from kernel to code proofs
1 parent 94f9a6b commit daa2673

File tree

2 files changed

+165
-110
lines changed

2 files changed

+165
-110
lines changed

lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,7 @@ object FOLHelpers {
120120
def asFront(cf: K.ConnectorFormula): Formula =
121121
cf.label match
122122
case K.And | K.Or if cf.args.size == 1 => asFront(cf.args(0))
123+
case K.And | K.Or => cf.args.map(asFront).reduceLeft((a, b) => asFrontLabel(cf.label)(Seq(a, b))) // TODO: handle this more gracefully
123124
case _ => asFrontLabel(cf.label).applyUnsafe(cf.args.map(asFront))
124125
def asFront(bf: K.BinderFormula): BinderFormula =
125126
asFrontLabel(bf.label).apply(asFrontLabel(bf.bound), asFront(bf.inner))

0 commit comments

Comments
 (0)