In [1]:
import $cp.bin.`provingground-core-jvm-e0f46c1def.fat.jar`
Out[1]:
In [2]:
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
Out[2]:
First we define some terms and types
In [3]:
val A = Type.sym
val B = Type.sym
val a = A.sym
val f = "f" :: A ->: B
val mp = a :-> (f :-> f(a))
Out[3]:
We derive equations and construct an expression evaluator
In [4]:
val de = new DerivedEquations
val tg = TermGenParams()
val ts = TermState(FiniteDistribution(), FiniteDistribution.unif(A, B))
val eqNodes = de.formalEquations(mp) union de.termStateInit(ts)
val ev = ExpressionEval.fromInitEqs(ts, Equation.group(eqNodes), tg)
Out[4]:
We check that we can generate mp
In [5]:
ev.finalTerms
Out[5]:
First conclusion: We successfully generated modus ponens depending on $A$ and $B$.
We next turn to Modus Ponens, but in its full (universal) form
In [6]:
val mpU = A :~> (B :~> mp)
val tsU = TermState(FiniteDistribution(), FiniteDistribution.unif(Type))
val eqNodesU = de.formalEquations(mpU) union de.termStateInit(tsU)
val evU = ExpressionEval.fromInitEqs(tsU, Equation.group(eqNodesU), tg)
evU.finalTerms
Out[6]: