In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
import $ivy.$
In [2]:
import provingground._ , interface._, HoTT._
import provingground.{FiniteDistribution => FD}
Out[2]:
import provingground._ , interface._, HoTT._

import provingground.{FiniteDistribution => FD}
In [3]:
val A = "A" :: Type
val B = "B" :: Type
val MP = A ~>: (B ~>: (A ->: (A ->: B) ->: B))
Out[3]:
A: Typ[Term] = SymbTyp(Name("A"), 0)
B: Typ[Term] = SymbTyp(Name("B"), 0)
MP: GenFuncTyp[Typ[Term], FuncLike[Typ[Term], Func[Term, Func[Func[Term, Term], Term]]]] = PiDefn(
  SymbTyp(A, 0),
  PiDefn(
    SymbTyp(B, 0),
    FuncTyp(
      SymbTyp(A, 0),
      FuncTyp(FuncTyp(SymbTyp(A, 0), SymbTyp(B, 0)), SymbTyp(B, 0))
    )
  )
)
In [4]:
repl.pprinter.bind(translation.FansiShow.fansiPrint)
In [5]:
import learning._
val tg = TermGenParams()
val mfd = MonixFiniteDistributionEq(tg.nodeCoeffSeq)
val ts = TermState(FD.unif(Type), FD.unif(Type), goals = FD.unif(MP))
Out[5]:
import learning._

tg: TermGenParams = TermGenParams(0.1, 0.1, 0.1, 0.1, 0.1, 0.05, 0.05, 0.05, 0.3, 0.5, 0.5)
mfd: MonixFiniteDistributionEq[TermState, Term] = MonixFiniteDistributionEq(
  Cons(
    BaseCons(
      BasePi(
        provingground.learning.RandomVarFamily$$Lambda$3765/1938135699@5621c319,
        FuncsWithDomain
      ),
      0.55,
      BaseCons(
        BasePi(
          provingground.learning.GeneratorNode$$Lambda$3768/328900033@1bd62afd,
          FuncsWithDomain
        ),
        0.1,
        BaseCons(
          BasePi(
            provingground.learning.GeneratorNode$$Lambda$3768/328900033@7cb1b783,
            FuncsWithDomain
          ),
          0.1,
          BaseCons(
            BasePi(
              provingground.learning.GeneratorNode$$Lambda$3768/328900033@50c609f4,
              FuncsWithDomain
            ),
            0.1,
            BaseCons(
              BasePi(
                provingground.learning.TermGeneratorNodes$$Lambda$3759/319800441@838a04e,
                FuncsWithDomain
              ),
              0.1,
              Target(FuncsWithDomain)
            )
          )
        )
      )
    ),
    Cons(
      BaseCons(
        Map(
          provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3771/1620514355@16c01a2,
          Goals,
          TargetTyps
        ),
        0.5,
        BaseCons(
          Map(
            provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3772/396853136@4062de80,
...
ts: TermState = TermState(
  FiniteDistribution(Vector(Weighted(š’° , 1.0))),
  FiniteDistribution(Vector(Weighted(š’° , 1.0))),
  Vector(),
  FiniteDistribution(Vector()),
  FiniteDistribution(Vector(Weighted(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }, 1.0))),
  Empty
)
In [6]:
import TermRandomVars._
val tsk = mfd.varDist(ts)(Terms, 0.00001)
import monix.execution.Scheduler.Implicits.global
Out[6]:
import TermRandomVars._

tsk: monix.eval.Task[(FiniteDistribution[Term], Set[GeneratorVariables.EquationTerm])] = FlatMap(
  Async(<function2>, true, true, true),
  monix.eval.Task$$Lambda$3893/194816733@4ed79980
)
import monix.execution.Scheduler.Implicits.global
In [7]:
val (fd, eqts) = tsk.runSyncUnsafe()
Out[7]:
fd: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((@a : (š’°  ā†’ š’° )) ā†¦ @a(@a), 2.5720562233697236E-4),
    Weighted((_ : @a) ā†¦ š’° , 3.3308015913189606E-4),
    Weighted((@a : āˆ(@a : š’° ){ š’° Ɨ@a }) ā†¦ @a, 1.868265711348081E-5),
    Weighted((@a : š’° ) ā†¦ (@a , @a), 5.088938816774152E-5),
    Weighted((((__1_1 , __1_2) , __2) : š’° Ɨš’° Ɨ(š’°  ā†’ š’° )) ā†¦ š’° , 1.6162528038990986E-5),
    Weighted((@a : š’° ) ā†¦ (_ : (š’°  ā†’ @a)) ā†¦ š’° , 5.7080968568555135E-5),
    Weighted((@a : š’° ) ā†¦ (_ : (@a ā†’ @a)) ā†¦ š’° , 3.4947531776666405E-5),
    Weighted((_ : š’° ) ā†¦ (_ : āˆ(@b : š’° ){ @b }) ā†¦ š’° , 8.15442408122216E-5),
    Weighted((_ : āˆ(@a : š’° ){ @a }) ā†¦ (_ : š’° ) ā†¦ š’° , 1.0972601302852661E-4),
    Weighted(
      (((@a_1_1 , @a_1_2) , @a_2) : (š’°  ā†’ š’° )Ɨš’° Ɨš’° ) ā†¦ ((@a_1_1 , @a_1_2) , @a_2),
      1.104989161849384E-5
    ),
    Weighted(
      ((@a_1 , (@a_2_1 , @a_2_2)) : š’° Ɨāˆ‘(@b : { @b }) ā†¦ (@a_1 , (@a_2_1 , @a_2_2)),
      1.7806741960864288E-5
    ),
    Weighted(((__1 , __2) : š’° Ɨ(š’°  ā†’ š’° )) ā†¦ š’° , 1.2838746108731833E-4),
    Weighted(((__1 , __2) : š’° Ɨ((š’°  ā†’ š’° ) ā†’ š’° )) ā†¦ š’° , 1.49785371268538E-5),
    Weighted((_ : š’° ) ā†¦ ((__1 , __2) : š’° Ɨš’° ) ā†¦ š’° , 7.434789406767466E-5),
    Weighted(((__1 , __2) : š’° Ɨš’° ) ā†¦ (_ : š’° ) ā†¦ š’° , 1.414581859196728E-4),
    Weighted(((@a_1 , @a_2) : āˆ‘(@a : { @a }) ā†¦ (@a_1 , @a_2), 2.706772538895482E-4),
    Weighted((@a : š’° ) ā†¦ ((__1 , __2) : āˆ‘(@b : { @b }) ā†¦ @a, 1.9508193778690146E-5),
    Weighted(((__1 , __2) : āˆ‘(@a : { @a }) ā†¦ (@a : š’° ) ā†¦ @a, 4.239700466872449E-5),
    Weighted(((@a_1 , @a_2) : (š’°  ā†’ š’° )Ɨ(š’°  ā†’ š’° )) ā†¦ (@a_1 , @a_2), 1.088914968823132E-5),
    Weighted((@a : āˆ(@a : š’° ){ @aƗ@a }) ā†¦ @a, 1.1438361498049473E-5),
    Weighted((@a : āˆ(@a : š’° ){ @a }) ā†¦ @a, 5.24912194961889E-5),
    Weighted(((__1 , __2) : š’° Ɨš’° ) ā†¦ @a, 7.039458036969333E-5),
    Weighted(
      ((@a_1 , (@a_2_1 , @a_2_2)) : āˆ‘(@a : { @aƗš’°  }) ā†¦ (@a_1 , (@a_2_1 , @a_2_2)),
      1.7806741960864288E-5
    ),
    Weighted((_ : š’° ) ā†¦ (@a : āˆ(@b : š’° ){ @b }) ā†¦ @a, 4.992504539523773E-5),
    Weighted((@a : āˆ(@a : š’° ){ @a }) ā†¦ (_ : š’° ) ā†¦ @a, 4.702543415508284E-5),
    Weighted((_ : (š’°  ā†’ š’° )) ā†¦ @a, 1.8499153661335303E-4),
    Weighted((_ : āˆ(@b : š’° ){ @b }) ā†¦ š’° , 0.0012864813449930822),
    Weighted(((__1 , (__2_1 , __2_2)) : š’° Ɨš’° Ɨš’° ) ā†¦ š’° , 6.786347213973834E-5),
    Weighted(š’° , 0.6842153844698987),
    Weighted((@a : š’° ) ā†¦ ((__1 , __2) : š’° Ɨ@a) ā†¦ @a, 1.3655735645083106E-5),
    Weighted(((__1 , (__2_1 , __2_2)) : āˆ‘(@a : { š’° Ɨ@a }) ā†¦ š’° , 2.9084345202745012E-5),
    Weighted((_ : @a) ā†¦ @a, 1.4274863962795541E-4),
    Weighted((_ : (š’°  ā†’ š’° )) ā†¦ (_ : (š’°  ā†’ š’° )) ā†¦ š’° , 3.527359991948709E-5),
    Weighted((@a : āˆ(@a : š’° ){ (@a ā†’ @a) }) ā†¦ @a, 4.1942359484037535E-5),
    Weighted((@a : (āˆ(@a : š’° ){ @a } ā†’ āˆ(@a : š’° ){ @a })) ā†¦ @a, 2.7907837998167127E-5),
    Weighted((@a : (š’°  ā†’ āˆ(@b : š’° ){ @b })) ā†¦ @a, 4.78123456776949E-5),
    Weighted((@a : āˆ(@a : š’° ){ (š’°  ā†’ @a) }) ā†¦ @a, 3.346864197438644E-5),
    Weighted((@a : š’° ) ā†¦ (_ : @a) ā†¦ (@a : @a) ā†¦ @a, 3.841128101966749E-5),
...
eqts: Set[GeneratorVariables.EquationTerm] = Set(
  EquationTerm(
    FinalVal(
      InIsle(
        Elem((@a : š’° ) ā†¦ @a, Terms),
        @a,
        Island(AtCoord(FuncsWithDomain, š’°  :: HNil), ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle)
      )
    ),
    Product(
      Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
      Product(
        Coeff(
          BaseThenCondition(
            FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
            Funcs,
            Restrict(FuncOpt)
          ),
          Funcs
        ),
        Product(
          Coeff(ZipMapOpt(UnifApplnOpt, Funcs, Terms, Terms), Terms),
          Product(
            Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
            FinalVal(
              InIsle(
                InIsle(
                  Elem(@a, Terms),
                  @a,
                  Island(Terms, ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle)
                ),
                @a,
                Island(
                  AtCoord(FuncsWithDomain, š’°  :: HNil),
                  ConstRandVar(Terms),
                  AddVar(š’° , 0.3),
                  Lambda,
                  InIsle
                )
              )
            )
          )
        )
      )
    )
  ),
  EquationTerm(
    FinalVal(
      InIsle(Elem(š’° , Typs), @a, Island(Terms, ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle))
...
In [8]:
fd.filter(_.typ == MP)
Out[8]:
res7: FiniteDistribution[Term] = FiniteDistribution(
  Vector(
    Weighted((@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), 0.027399963852253788)
  )
)
In [9]:
val eqs = GeneratorVariables.Equation.group(eqts)
Out[9]:
eqs: Set[GeneratorVariables.Equation] = Set(
  Equation(
    FinalVal(
      InIsle(
        InIsle(
          Elem(š’° , Terms),
          @b,
          Island(Terms, ConstRandVar(Terms), AddVar((š’°  ā†’ š’° ), 0.3), Lambda, InIsle)
        ),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar((š’°  ā†’ š’° ), 0.3), Lambda, InIsle)
      )
    ),
    Product(
      Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
      Product(
        Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
        Product(
          Coeff(Init(Terms), Terms),
          InitialVal(
            InIsle(
              InIsle(
                Elem(š’° , Terms),
                @b,
                Island(Terms, ConstRandVar(Terms), AddVar((š’°  ā†’ š’° ), 0.3), Lambda, InIsle)
              ),
              @a,
              Island(Terms, ConstRandVar(Terms), AddVar((š’°  ā†’ š’° ), 0.3), Lambda, InIsle)
            )
          )
        )
      )
    )
  ),
  Equation(
    InitialVal(
      InIsle(
        InIsle(
          Elem(@a, Terms),
          (@a_1 , @a_2),
          Island(Terms, ConstRandVar(Terms), AddVar(āˆ‘(@a : { @a }, 0.3), Lambda, InIsle)
        ),
        @a,
        Island(AtCoord(FuncsWithDomain, š’°  :: HNil), ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle)
      )
    ),
    Product(
      Coeff(FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms), Terms),
      Product(
...
In [10]:
import TermRandomVars._
Out[10]:
import TermRandomVars._
In [11]:
val mpProof = fd.support.find(_.typ == MP).get
Out[11]:
mpProof: Term = (@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a)
In [12]:
import GeneratorVariables._, Expression._
val pfVal = FinalVal(Elem(mpProof, Terms))
Out[12]:
import GeneratorVariables._

pfVal: FinalVal[Term] = FinalVal(
  Elem((@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms)
)
In [13]:
val mpEqs = eqs.find(_.lhs == pfVal)
Out[13]:
mpEqs: Option[Equation] = Some(
  Equation(
    FinalVal(Elem((@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms)),
    Sum(
      Sum(
        Product(
          Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
          Product(
            FinalVal(Elem(š’° , Typs)),
            FinalVal(Elem((@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms))
          )
        ),
        Product(
          Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
          Product(
            FinalVal(Elem(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }, TargetTyps)),
            FinalVal(
              Elem(
                (@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a),
                AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil)
              )
            )
          )
        )
      ),
      Product(
        Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
        FinalVal(
          InIsle(
            Elem((@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms),
            @a,
            Island(Terms, ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle)
          )
        )
      )
    )
  )
)
In [14]:
val mpEqTerms =  Expression.sumTerms(mpEqs.get.rhs)
Out[14]:
mpEqTerms: Vector[Expression] = Vector(
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
    Product(
      FinalVal(Elem(š’° , Typs)),
      FinalVal(Elem((@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms))
    )
  ),
  Product(
    Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
    Product(
      FinalVal(Elem(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }, TargetTyps)),
      FinalVal(
        Elem(
          (@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a),
          AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil)
        )
      )
    )
  ),
  Product(
    Coeff(FlatMap(Typs, LambdaIsle, Terms), Terms),
    FinalVal(
      InIsle(
        Elem((@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a), Terms),
        @a,
        Island(Terms, ConstRandVar(Terms), AddVar(š’° , 0.3), Lambda, InIsle)
      )
    )
  )
)
In [15]:
mpEqTerms.size
Out[15]:
res14: Int = 3
In [16]:
val ats = eqs.map(_.rhs).flatMap(Expression.atoms)
Out[16]:
ats: Set[Expression] = Set(
  InitialVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
            Elem(@b, Terms),
            @a,
            Island(
              AtCoord(FuncsWithDomain, š’°  :: HNil),
              ConstRandVar(Terms),
              AddVar(š’° , 0.3),
              Lambda,
              InIsle
            )
          ),
          @a,
          Island(
            AtCoord(TermsWithTyp, (@a ā†’ ((@a ā†’ @b) ā†’ @b)) :: HNil),
            ConstRandVar(AtCoord(TermsWithTyp, ((@a ā†’ @b) ā†’ @b) :: HNil)),
            AddVar(@a, 0.3),
            Lambda,
            InIsle
          )
        ),
        @b,
        Island(
          AtCoord(TermsWithTyp, āˆ(B : š’° ){ (@a ā†’ ((@a ā†’ B) ā†’ B)) } :: HNil),
          PiOutput(āˆ(B : š’° ){ (@a ā†’ ((@a ā†’ B) ā†’ B)) }),
          AddVar(š’° , 0.3),
          Lambda,
          InIsle
        )
      ),
      @a,
      Island(
        AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil),
        PiOutput(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }),
        AddVar(š’° , 0.3),
        Lambda,
        InIsle
      )
    )
  ),
  FinalVal(
    InIsle(
      InIsle(
        InIsle(
          InIsle(
...
In [17]:
val coeffs = ats.collect{case coeff @ Coeff(_, _) => coeff}
Out[17]:
coeffs: Set[Coeff[Any]] = Set(
  Coeff(
    BaseThenCondition(ZipMapOpt(UnifApplnOpt, TypFamilies, Terms, Terms), Typs, Restrict(TypOpt)),
    Typs
  ),
  Coeff(BaseThenCondition(FlatMap(Typs, LambdaIsle, Terms), Funcs, Restrict(FuncOpt)), Funcs),
  Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms),
      Funcs,
      Restrict(FuncOpt)
    ),
    Funcs
  ),
  Coeff(
    BaseThenCondition(
      FiberProductMap(domOf, TermsWithTyp, Appln, TypFamilies, Terms),
      TypFamilies,
      Restrict(TypFamilyOpt)
    ),
    TypFamilies
  ),
  Coeff(
    FlatMap(Typs, provingground.learning.TermGeneratorNodes$$Lambda$3760/965851966@772ff1b1, Typs),
    Typs
  ),
  Coeff(Init(Goals), Goals),
  Coeff(FlatMap(Typs, LambdaTypFamilyIsle, TypFamilies), TypFamilies),
  Coeff(
    Map(
      provingground.learning.TermRandomVars$TargetTyps$$$Lambda$3771/1620514355@16c01a2,
      Goals,
      TargetTyps
    ),
    TargetTyps
  ),
  Coeff(
    BaseThenCondition(
      FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms),
      Funcs,
      Restrict(FuncOpt)
    ),
    Funcs
  ),
  Coeff(FiberProductMap(typeOf(_), FuncsWithDomain, FlipAppn, Terms, Terms), Terms),
  Coeff(FiberProductMap(domOf, TermsWithTyp, Appln, Funcs, Terms), Terms),
  Coeff(Init(Terms), Terms),
  Coeff(Init(TypFamilies), TypFamilies),
...
In [18]:
val cs =  coeffs.toVector.map(c => c.get(tg.nodeCoeffSeq) -> c.rv)
Out[18]:
cs: Vector[(Option[Double], RandomVar[Any])] = Vector(
  (Some(0.1), Typs),
  (Some(0.1), Funcs),
  (Some(0.05), Terms),
  (Some(0.1), Funcs),
  (Some(0.1), TypFamilies),
  (Some(0.1), Typs),
  (Some(1.0), Goals),
  (Some(0.1), TypFamilies),
  (Some(0.5), TargetTyps),
  (Some(0.1), Funcs),
  (Some(0.1), Terms),
  (Some(0.1), Terms),
  (Some(0.55), Terms),
  (Some(0.55), TypFamilies),
  (Some(0.1), Terms),
  (Some(0.1), Typs),
  (Some(0.1), Terms),
  (Some(0.05), Typs),
  (Some(0.1), Funcs),
  (Some(0.05), Funcs),
  (Some(0.55), Funcs),
  (Some(0.5), TargetTyps),
  (Some(0.1), TypFamilies),
  (Some(0.05), Typs),
  (Some(0.05), TypFamilies),
  (Some(0.1), TypFamilies),
  (Some(0.5), TypsAndFamilies),
  (Some(0.6), Typs),
  (Some(0.5), TypsAndFamilies)
)
In [21]:
val target = Expression.varVals(mpEqTerms(1)).tail.head
Out[21]:
target: VarVal[Any] = FinalVal(
  Elem(
    (@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a),
    AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil)
  )
)
In [27]:
val teqs = eqs.filter(_.lhs == target)
Out[27]:
teqs: Set[Equation] = Set(
  Equation(
    FinalVal(
      Elem(
        (@a : š’° ) ā†¦ (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a),
        AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil)
      )
    ),
    Product(
      Coeff(ZipFlatMap(TargetTyps, TermsWithTyp, Proj2, Terms), Terms),
      FinalVal(
        InIsle(
          Elem(
            (@b : š’° ) ā†¦ (@a : @a) ā†¦ (@a : (@a ā†’ @b)) ā†¦ @a(@a),
            AtCoord(TermsWithTyp, āˆ(B : š’° ){ (@a ā†’ ((@a ā†’ B) ā†’ B)) } :: HNil)
          ),
          @a,
          Island(
            AtCoord(TermsWithTyp, āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } } :: HNil),
            PiOutput(āˆ(A : š’° ){ āˆ(B : š’° ){ (A ā†’ ((A ā†’ B) ā†’ B)) } }),
            AddVar(š’° , 0.3),
            Lambda,
            InIsle
          )
        )
      )
    )
  )
)
In [28]:
teqs.size
Out[28]:
res27: Int = 1
In [ ]:
In [ ]: