Lean2Js . Builder

(name : String) :

Equations

Lean2Js.Core.Builder.v name = Lean2Js.Core.Expr.var name

Instances For

Used by

def

Lean2Js.Core.Builder.bool

(b : Bool) :

Equations

Lean2Js.Core.Builder.bool b = Lean2Js.Core.Expr.lit (Lean2Js.Core.Lit.bool b)

Instances For

Used by

def

Lean2Js.Core.Builder.int53

(i : Int) :

Equations

Lean2Js.Core.Builder.int53 i = Lean2Js.Core.Expr.lit (Lean2Js.Core.Lit.int53 i)

Instances For

Used by

def

Lean2Js.Core.Builder.uint32

(n : UInt32) :

Equations

Lean2Js.Core.Builder.uint32 n = Lean2Js.Core.Expr.lit (Lean2Js.Core.Lit.uint32 n)

Instances For

Used by

def

Lean2Js.Core.Builder.str

(s : String) :

Equations

Lean2Js.Core.Builder.str s = Lean2Js.Core.Expr.lit (Lean2Js.Core.Lit.str s)

Instances For

Used by

def

Lean2Js.Core.Builder.bigint

(i : Int) :

Equations

Lean2Js.Core.Builder.bigint i = Lean2Js.Core.Expr.lit (Lean2Js.Core.Lit.bigint i)

Instances For

Used by

def

Lean2Js.Core.Builder.«term_+'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_-'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_*'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_/'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_%'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_++'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_<'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_≤'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_>'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_≥'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_=='_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_≠'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_&&'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.«term_||'_»

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

def

Lean2Js.Core.Builder.not'

(e : Expr) :

Equations

Lean2Js.Core.Builder.not' e = Lean2Js.Core.Expr.un Lean2Js.Core.UnOp.not e

Instances For

Used by

def

Lean2Js.Core.Builder.neg'

(e : Expr) :

Equations

Lean2Js.Core.Builder.neg' e = Lean2Js.Core.Expr.un Lean2Js.Core.UnOp.neg e

Instances For

Used by

def

Lean2Js.Core.Builder.abs'

(e : Expr) :

Equations

Lean2Js.Core.Builder.abs' e = Lean2Js.Core.Expr.un Lean2Js.Core.UnOp.abs e

Instances For

Used by

def

Lean2Js.Core.Builder.toString'

(e : Expr) :

Equations

Lean2Js.Core.Builder.toString' e = Lean2Js.Core.Expr.un Lean2Js.Core.UnOp.toString e

Instances For

Used by

def

Lean2Js.Core.Builder.range'

(e : Expr) :

Equations

Lean2Js.Core.Builder.range' e = Lean2Js.Core.Expr.un Lean2Js.Core.UnOp.range e

Instances For

Used by

def

Lean2Js.Core.Builder.min'

(a b : Expr) :

Equations

Lean2Js.Core.Builder.min' a b = Lean2Js.Core.Expr.bin Lean2Js.Core.BinOp.min a b

Instances For

Used by

def

Lean2Js.Core.Builder.max'

(a b : Expr) :

Equations

Lean2Js.Core.Builder.max' a b = Lean2Js.Core.Expr.bin Lean2Js.Core.BinOp.max a b

Instances For

Used by

def

Lean2Js.Core.Builder.fnRef

(name : String) :

Equations

Lean2Js.Core.Builder.fnRef name = Lean2Js.Core.Expr.fnRef name

Instances For

Used by

def

Lean2Js.Core.Builder.ite'

(c t e : Expr) :

Equations

Lean2Js.Core.Builder.ite' c t e = c.cond t e

Instances For

Used by

def

Lean2Js.Core.Builder.letIn

(name : String) (ty : Ty) (val body : Expr) :

Equations

Lean2Js.Core.Builder.letIn name ty val body = Lean2Js.Core.Expr.letE name ty val body

Instances For

Used by

def

Lean2Js.Core.Builder.call

(fn : String) (args : List Expr) :

Equations

Lean2Js.Core.Builder.call fn args = Lean2Js.Core.Expr.call fn args

Instances For

Used by

def

Lean2Js.Core.Builder.ctor

(typeName : String) (tyArgs : List Ty) (ctorName : String) (args : List Expr) :

Equations

Lean2Js.Core.Builder.ctor typeName tyArgs ctorName args = Lean2Js.Core.Expr.ctor typeName tyArgs ctorName args

Instances For

Used by

def

Lean2Js.Core.Builder.proj

(e : Expr) (field : String) :

Equations

Lean2Js.Core.Builder.proj e field = e.proj field

Instances For

Used by

def

Lean2Js.Core.Builder.matchOn

(scrut : Expr) (alts : List Alt) :

Equations

Lean2Js.Core.Builder.matchOn scrut alts = scrut.matchE alts

Instances For

Used by

def

Lean2Js.Core.Builder.none'

(elem : Ty) :

Equations

Lean2Js.Core.Builder.none' elem = Lean2Js.Core.Expr.noneE elem

Instances For

Used by

def

Lean2Js.Core.Builder.some'

(e : Expr) :

Equations

Lean2Js.Core.Builder.some' e = e.someE

Instances For

Used by

def

Lean2Js.Core.Builder.ok'

(err : Ty) (e : Expr) :

Equations

Lean2Js.Core.Builder.ok' err e = Lean2Js.Core.Expr.okE err e

Instances For

Used by

def

Lean2Js.Core.Builder.error'

(ok : Ty) (e : Expr) :

Equations

Lean2Js.Core.Builder.error' ok e = Lean2Js.Core.Expr.errorE ok e

Instances For

Used by

def

Lean2Js.Core.Builder.array

(elem : Ty) (items : List Expr) :

Equations

Lean2Js.Core.Builder.array elem items = Lean2Js.Core.Expr.arrayLit elem items

Instances For

Used by

def

Lean2Js.Core.Builder.at'

(arr idx : Expr) :

Equations

Lean2Js.Core.Builder.at' arr idx = arr.index idx

Instances For

Used by

def

Lean2Js.Core.Builder.len

(arr : Expr) :

Equations

Lean2Js.Core.Builder.len arr = arr.length

Instances For

Used by

def

Lean2Js.Core.Builder.arraySlice

(arr lo hi : Expr) :

Equations

Lean2Js.Core.Builder.arraySlice arr lo hi = arr.arraySlice lo hi

Instances For

Used by

def

Lean2Js.Core.Builder.arrayReverse

(arr : Expr) :

Equations

Lean2Js.Core.Builder.arrayReverse arr = arr.arrayReverse

Instances For

Used by

def

Lean2Js.Core.Builder.map'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.map' arr binder body = arr.mapE binder body

Instances For

Used by

def

Lean2Js.Core.Builder.filter'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.filter' arr binder body = arr.filterE binder body

Instances For

Used by

def

Lean2Js.Core.Builder.sortByKey'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.sortByKey' arr binder body = arr.sortByKeyE binder body

Instances For

Used by

def

Lean2Js.Core.Builder.find'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.find' arr binder body = arr.findE binder body

Instances For

Used by

def

Lean2Js.Core.Builder.all'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.all' arr binder body = Lean2Js.Core.Expr.quantE Lean2Js.Core.QuantOp.all arr binder body

Instances For

Used by

def

Lean2Js.Core.Builder.any'

(arr : Expr) (binder : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.any' arr binder body = Lean2Js.Core.Expr.quantE Lean2Js.Core.QuantOp.any arr binder body

Instances For

Used by

def

Lean2Js.Core.Builder.reduce'

(arr init : Expr) (accName elemName : String) (body : Expr) :

Equations

Lean2Js.Core.Builder.reduce' arr init accName elemName body = arr.reduceE init accName elemName body

Instances For

Used by

def

Lean2Js.Core.Builder.dict

(value : Ty) (entries : List (String × Expr)) :

Equations

Lean2Js.Core.Builder.dict value entries = Lean2Js.Core.Expr.dictLit value false entries

Instances For

Used by

def

Lean2Js.Core.Builder.dictGet

(d key : Expr) :

Equations

Lean2Js.Core.Builder.dictGet d key = d.dictGet key

Instances For

Used by

def

Lean2Js.Core.Builder.dictHas

(d key : Expr) :

Equations

Lean2Js.Core.Builder.dictHas d key = d.dictHas key

Instances For

Used by

def

Lean2Js.Core.Builder.dictSet

(d key val : Expr) :

Equations

Lean2Js.Core.Builder.dictSet d key val = d.dictSet key val

Instances For

Used by

def

Lean2Js.Core.Builder.dictKeys

(d : Expr) :

Equations

Lean2Js.Core.Builder.dictKeys d = d.dictKeys

Instances For

Used by

def

Lean2Js.Core.Builder.dictValues

(d : Expr) :

Equations

Lean2Js.Core.Builder.dictValues d = d.dictValues

Instances For

Used by

def

Lean2Js.Core.Builder.dictDelete

(d key : Expr) :

Equations

Lean2Js.Core.Builder.dictDelete d key = d.dictDelete key

Instances For

Used by

def

Lean2Js.Core.Builder.trim

(e : Expr) :

Equations

Lean2Js.Core.Builder.trim e = Lean2Js.Core.Expr.strUn Lean2Js.Core.StrUnOp.trim e

Instances For

Used by

def

Lean2Js.Core.Builder.upper

(e : Expr) :

Equations

Lean2Js.Core.Builder.upper e = Lean2Js.Core.Expr.strUn Lean2Js.Core.StrUnOp.upper e

Instances For

Used by

def

Lean2Js.Core.Builder.lower

(e : Expr) :

Equations

Lean2Js.Core.Builder.lower e = Lean2Js.Core.Expr.strUn Lean2Js.Core.StrUnOp.lower e

Instances For

Used by

def

Lean2Js.Core.Builder.toInt

(e : Expr) :

Equations

Lean2Js.Core.Builder.toInt e = Lean2Js.Core.Expr.strUn Lean2Js.Core.StrUnOp.toInt e

Instances For

Used by

def

Lean2Js.Core.Builder.startsWith

(s prefix' : Expr) :

Equations

Lean2Js.Core.Builder.startsWith s prefix' = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.startsWith s prefix'

Instances For

Used by

def

Lean2Js.Core.Builder.indexOf

(s needle : Expr) :

Equations

Lean2Js.Core.Builder.indexOf s needle = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.indexOf s needle

Instances For

Used by

def

Lean2Js.Core.Builder.join

(xs sep : Expr) :

Equations

Lean2Js.Core.Builder.join xs sep = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.join xs sep

Instances For

Used by

def

Lean2Js.Core.Builder.repeat

(s n : Expr) :

Equations

Lean2Js.Core.Builder.repeat s n = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.repeat s n

Instances For

Used by

def

Lean2Js.Core.Builder.endsWith

(s suffix : Expr) :

Equations

Lean2Js.Core.Builder.endsWith s suffix = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.endsWith s suffix

Instances For

Used by

def

Lean2Js.Core.Builder.includes

(s needle : Expr) :

Equations

Lean2Js.Core.Builder.includes s needle = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.includes s needle

Instances For

Used by

def

Lean2Js.Core.Builder.split

(s sep : Expr) :

Equations

Lean2Js.Core.Builder.split s sep = Lean2Js.Core.Expr.strBin Lean2Js.Core.StrBinOp.split s sep

Instances For

Used by

def

Lean2Js.Core.Builder.substring

(s lo hi : Expr) :

Equations

Lean2Js.Core.Builder.substring s lo hi = s.substring lo hi

Instances For

Used by

def

Lean2Js.Core.Builder.foldOn

(scrut : Expr) (typeName : String) (tyArgs : List Ty) (result : Ty) (alts : List Alt) :