In [18]:

    

import $ivy.`in.ac.iisc::provingground-core:0.1.0`


    

    
Out[18]:





import $ivy.$                                            

In [ ]:

    




    

In [19]:

    

import provingground._, functionfinder._


    

    
Out[19]:





import provingground._, functionfinder._

In [20]:

    

import spire.math._


    

    
Out[20]:





import spire.math._

In [21]:

    

1 : SafeLong


    

    
Out[21]:





res20: SafeLong = 1

In [22]:

    

import NatRing._


    

    
Out[22]:





import NatRing._

In [23]:

    

1 : Nat


    

    
Out[23]:





res22: Nat = ScalaSymbol(1) : (Nat.Typ)

In [24]:

    

import HoTT._
val A = "A" :: Type
val B = "B" :: Type


    

    
Out[24]:





import HoTT._

A: Typ[Term] with Subs[Typ[Term]] = A : 𝒰 _0
B: Typ[Term] with Subs[Typ[Term]] = B : 𝒰 _0

In [25]:

    

val a ="a" :: A
val f ="f" :: A ->: B
val mp = lambda(A)(lambda(B)(lmbda(a)(lmbda(f)(f(a)))))


    

    
Out[25]:





a: Term with Subs[Term] = a : (A : 𝒰 _0)
f: Func[Term, Term] with Subs[Func[Term, Term]] = f : ((A : 𝒰 _0) → (B : 𝒰 _0))
mp: FuncLike[Typ[Term] with Subs[Typ[Term]], FuncLike[Typ[Term] with Subs[Typ[Term]], Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]]]] = (A : 𝒰 _0) ↦ ((B : 𝒰 _0) ↦ ((a : (A : 𝒰 _0)) ↦ ((f : ((A : 𝒰 _0) → (B : 𝒰 _0))) ↦ ((f : ((A : 𝒰 _0) → (B : 𝒰 _0))) (a : (A : 𝒰 _0)) : (B : 𝒰 _0)))))

In [26]:

    

val mpPf = mp(B)(A)


    

    
Out[26]:





mpPf: Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]] = (a : (B : 𝒰 _0)) ↦ ((f : ((B : 𝒰 _0) → (A : 𝒰 _0))) ↦ ((f : ((B : 𝒰 _0) → (A : 𝒰 _0))) (a : (B : 𝒰 _0)) : (A : 𝒰 _0)))

In [27]:

    

mpPf.typ


    

    
Out[27]:





res26: Typ[Func[Term with Subs[Term], Func[Func[Term, Term] with Subs[Func[Term, Term]], Term]]] = (B : 𝒰 _0) → (((B : 𝒰 _0) → (A : 𝒰 _0)) → (A : 𝒰 _0))

In [ ]: