Skip to content

Lean2Js.Example

Imports 8

Business logic written in Lean, and the theorems proved about it #

Ordinary Lean defs, each marked @[ship], and the theorems proved about them. Marking a def reads a declaration out of it, and ship_package gathers them into the program and writes the proof that each declaration denotes the def it was read from.

The program placed here is what ships as packages/verified-example.

def

Lean2Js.Example.add

(a b : Int) :

Equations

Lean2Js.Example.add a b = a + b

Instances For

Used by

def

Lean2Js.Example.clampQuantity

(quantity upper : Int) :

Clamps a quantity to at least 1 and at most upper.

Equations

Lean2Js.Example.clampQuantity quantity upper = if quantity < 1 then 1 else if quantity > upper then upper else quantity

Instances For

Used by

def

Lean2Js.Example.maxLineQuantity

:

The most of one line a single order is billed for.

Equations

Lean2Js.Example.maxLineQuantity = 999

Instances For

Used by

def

Lean2Js.Example.lineTotal

(unitPrice quantity : Int) :

The amount of a line item. The quantity is clamped before multiplying, so a negative quantity never makes the amount negative.

Equations

Lean2Js.Example.lineTotal unitPrice quantity = unitPrice * Lean2Js.Example.clampQuantity quantity Lean2Js.Example.maxLineQuantity

Instances For

Used by

inductive

Lean2Js.Example.Role

:

guest : Role
member : Role
admin : Role

Instances For

Used by

def

Lean2Js.Example.Role.typeDef

:

Equations

Lean2Js.Example.Role.typeDef = { name := "Role", ctors := [{ name := "guest", fields := [] }, { name := "member", fields := [] }, { name := "admin", fields := [] }] }

Instances For

Used by

def

Lean2Js.Example.Role.ofValue

(v : Value) :

Equations

Instances For

Used by

theorem

Lean2Js.Example.Role.ofValue_toValue

(x : Role) :

ofValue x.toValue = some x

Used by

theorem

Lean2Js.Example.Role.toValue_eq

@[simp]

:

Enc.toValue = toValue

Used by

instance

Lean2Js.Example.instEncRole

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Example.Role.toValue_hasTy

{p : Core.Program} {x : Role} :

accepts p x → Value.hasTy p x.toValue (Core.Ty.named "Role" []) = true

Used by

theorem

Lean2Js.Example.Role.ty_eq

@[simp]

:

Enc.ty Role = Core.Ty.named "Role" []

Used by

def

Lean2Js.Example.Role.accepts

(p : Core.Program) (x : Role) :

Equations

Instances For

Used by

def

Lean2Js.Example.Role.toValue

(x : Role) :

Equations

Lean2Js.Example.Role.guest.toValue = Lean2Js.Value.obj "guest" []
Lean2Js.Example.Role.member.toValue = Lean2Js.Value.obj "member" []
Lean2Js.Example.Role.admin.toValue = Lean2Js.Value.obj "admin" []

Instances For

Used by

def

Lean2Js.Example.roleRank

(role : Role) :

Equations

Instances For

Used by

def

Lean2Js.Example.lineTotals

(unitPrice : Int) (quantities : List Int) :

The amount of every line of an order at one unit price.

Equations

Lean2Js.Example.lineTotals unitPrice quantities = List.map (fun (quantity : Int) => Lean2Js.Example.lineTotal unitPrice quantity) quantities

Instances For

Used by

def

Lean2Js.Example.anyOverLimit

(amounts : List Int) (limit : Int) :

Equations

Lean2Js.Example.anyOverLimit amounts limit = List.foldl (fun (seen : Bool) (amount : Int) => if seen = true then true else decide (amount > limit)) false amounts

Instances For

Used by

def

Lean2Js.Example.firstOverLimit

(amounts : List Int) (limit : Int) :

The first line that breaks the limit. Lines after it are never looked at.

Equations

Lean2Js.Example.firstOverLimit amounts limit = List.find? (fun (amount : Int) => decide (amount > limit)) amounts

Instances For

Used by

def

Lean2Js.Example.everyLineWithinLimit

(amounts : List Int) (limit : Int) :

Equations

Lean2Js.Example.everyLineWithinLimit amounts limit = amounts.all fun (amount : Int) => decide (amount ≤ limit)

Instances For

Used by

def

Lean2Js.Example.someLineIsFree

(amounts : List Int) :

Equations

Lean2Js.Example.someLineIsFree amounts = amounts.any fun (amount : Int) => amount == 0

Instances For

Used by

def

Lean2Js.Example.pageOf

(xs : List Int) (lo hi : Int) :

One window of a list. A window reaching past the end is refused rather than shortened.

Equations

Lean2Js.Example.pageOf xs lo hi = Lean2Js.Arr.slice xs lo hi

Instances For

Used by

def

Lean2Js.Example.mostRecentFirst

(events : List String) :

Equations

Lean2Js.Example.mostRecentFirst events = events.reverse

Instances For

Used by

def

Lean2Js.Example.combinedCart

(saved added : List Int) :

Equations

Lean2Js.Example.combinedCart saved added = saved ++ added

Instances For

Used by

def

Lean2Js.Example.headOr

(xs : List Int) (fallback : Int) :

An out-of-range read traps rather than yielding undefined.

Equations

Lean2Js.Example.headOr xs fallback = if Lean2Js.Arr.length xs < 1 then fallback else Lean2Js.Arr.get xs 0

Instances For

Used by

def

Lean2Js.Example.slugOf

(«prefix» name : String) :

Equations

Lean2Js.Example.slugOf «prefix» name = «prefix» ++ "-" ++ name

Instances For

Used by

def

Lean2Js.Example.orderReference

(«prefix» : String) (orderNo : Int) :

The reference an order is filed under: the prefix and the order number in decimal.

Equations

Lean2Js.Example.orderReference «prefix» orderNo = «prefix» ++ "-" ++ Lean2Js.Int53.toString orderNo

Instances For

Used by

def

Lean2Js.Example.amountOf

(field : String) :

The amount a line carries, read back from the string the caller was handed. none unless the string is exactly the decimal spelling of an Int53, so "007", " 5" and "+5" are refused.

Equations

Lean2Js.Example.amountOf field = Lean2Js.Str.toInt? field

Instances For

Used by

def

Lean2Js.Example.amountOr

(field : String) (fallback : Int) :

The same amount, with a fallback for a field that does not spell one.

Equations

Lean2Js.Example.amountOr field fallback = Lean2Js.Opt.getD (Lean2Js.Str.toInt? field) fallback

Instances For

Used by

def

Lean2Js.Example.separatorAt

(reference sep : String) :

Where the separator first sits in a reference, counted in code points. none when the reference carries none. JS's own indexOf counts UTF-16 units and answers -1.

Equations

Lean2Js.Example.separatorAt reference sep = Lean2Js.Str.indexOf? reference sep

Instances For

Used by

def

Lean2Js.Example.referencePrefix

(reference : String) :

The part of a reference before its first separator, or the whole reference when it carries none.

Equations

Lean2Js.Example.referencePrefix reference = match Lean2Js.Str.indexOf? reference "-" with | some i => Lean2Js.Str.substring reference 0 i | none => reference

Instances For

Used by

def

Lean2Js.Example.joinFields

(fields : List String) (separator : String) :

A row of an uploaded file written back out: the fields in order with the separator between them. An empty list of fields writes an empty row.

Equations

Lean2Js.Example.joinFields fields separator = Lean2Js.Str.join fields separator

Instances For

Used by

def

Lean2Js.Example.referenceFrom

(parts : List String) :

The reference an order is filed under, built from parts that are already in hand, under the same separator referencePrefix reads back.

Equations

Lean2Js.Example.referenceFrom parts = Lean2Js.Str.join parts "-"

Instances For

Used by

def

Lean2Js.Example.refiled

(reference oldSep newSep : String) :

A reference filed under one separator, rewritten under another. Every occurrence moves, and a reference carrying none comes back unchanged.

Equations

Lean2Js.Example.refiled reference oldSep newSep = Lean2Js.Str.replace reference oldSep newSep

Instances For

Used by

def

Lean2Js.Example.receiptRule

(mark : String) :

The rule a printed receipt puts between its sections: mark written out 32 times, which is one column each where mark is a single character.

Equations

Lean2Js.Example.receiptRule mark = Lean2Js.Str.repeat mark 32

Instances For

Used by

def

Lean2Js.Example.amountColumn

(amount : Int) :

An amount in minor units, right-aligned in the column a printed receipt gives it. Too wide an amount keeps its digits and overruns the column.

Equations

Lean2Js.Example.amountColumn amount = Lean2Js.Str.padStart (Lean2Js.Int53.toString amount) 12 " "

Instances For

Used by

def

Lean2Js.Example.maxReceiptRows

:

The most rows a single printed receipt numbers.

Equations

Lean2Js.Example.maxReceiptRows = 999

Instances For

Used by

def

Lean2Js.Example.lineNumbers

(rows : Int) :

The line numbers a printed receipt gives its rows, counting from one. The count is clamped: a receipt prints at most maxReceiptRows rows, and Arr.range asks that the text bound how far it counts.

Equations

Lean2Js.Example.lineNumbers rows = List.map (fun (i : Int) => i + 1) (Lean2Js.Arr.range (min (max rows 0) Lean2Js.Example.maxReceiptRows))

Instances For

Used by

def

Lean2Js.Example.sortsBefore

(a b : String) :

Comparison in code point order. JS's < compares UTF-16 units, so it does not agree.

Equations

Lean2Js.Example.sortsBefore a b = decide (a < b)

Instances For

Used by

def

Lean2Js.Example.mentionsTerm

(text term : String) :

Whether a free-text note mentions a search term, ignoring case.

Equations

Lean2Js.Example.mentionsTerm text term = Lean2Js.Str.includes (Lean2Js.Str.lower text) (Lean2Js.Str.lower term)

Instances For

Used by

def

Lean2Js.Example.storedCoupon

(campaign entered : String) :

A coupon code as it is stored: the campaign prefix and what the customer typed, upper-cased and with the surrounding whitespace gone.

Equations

Lean2Js.Example.storedCoupon campaign entered = Lean2Js.Str.upper (Lean2Js.Str.trim (campaign ++ entered))

Instances For

Used by

def

Lean2Js.Example.comparable

(s : String) :

The spelling two strings are compared under: the surrounding whitespace gone and the case levelled. Every comparison below goes through it and no consumer has any business calling it, which is what @[ship internal] says — it is compiled and called like any other declaration, and appears in neither index.d.ts nor the exports of index.js.

Equations

Lean2Js.Example.comparable s = Lean2Js.Str.lower (Lean2Js.Str.trim s)

Instances For

Used by

def

Lean2Js.Example.couponApplies

(code campaign : String) :

Whether a coupon belongs to a campaign, comparing the way the codes are stored.

Equations

Lean2Js.Example.couponApplies code campaign = Lean2Js.Str.startsWith (Lean2Js.Example.comparable code) (Lean2Js.Example.comparable campaign)

Instances For

Used by

def

Lean2Js.Example.fieldCount

(row separator : String) :

How many columns a line of an uploaded file carries. An empty separator leaves the line whole rather than cutting it into characters.

Equations

Lean2Js.Example.fieldCount row separator = Lean2Js.Arr.length (Lean2Js.Str.split row separator)

Instances For

Used by

def

Lean2Js.Example.truncateLabel

(label : String) (limit : Int) :

A label cut to fit, counted in code points so a surrogate pair is never split in half. A negative limit has no string to return and fails the way an out-of-range index does.

Equations

Lean2Js.Example.truncateLabel label limit = if Lean2Js.Str.length label ≤ limit then label else Lean2Js.Str.substring label 0 limit ++ "..."

Instances For

Used by

def

Lean2Js.Example.isSpreadsheet

(fileName : String) :

Whether an uploaded file is a spreadsheet, compared the way the names are stored.

Equations

Lean2Js.Example.isSpreadsheet fileName = Lean2Js.Str.endsWith (Lean2Js.Example.comparable fileName) ".csv"

Instances For

Used by

def

Lean2Js.Example.limitsFor

(role : Role) :

What a role may do in a day and in a month.

Equations

Lean2Js.Example.limitsFor Lean2Js.Example.Role.guest = Lean2Js.Dict.ofList [("daily", 10), ("monthly", 100)]
Lean2Js.Example.limitsFor Lean2Js.Example.Role.member = Lean2Js.Dict.ofList [("daily", 100), ("monthly", 3000)]
Lean2Js.Example.limitsFor Lean2Js.Example.Role.admin = Lean2Js.Dict.ofList [("daily", 1000), ("monthly", 30000)]

Instances For

Used by

def

Lean2Js.Example.priceOf

(prices : Dict Int) (sku : String) :

Equations

Lean2Js.Example.priceOf prices sku = prices.get sku

Instances For

Used by

def

Lean2Js.Example.isListed

(prices : Dict Int) (sku : String) :

Equations

Lean2Js.Example.isListed prices sku = prices.has sku

Instances For

Used by

def

Lean2Js.Example.repriced

(prices : Dict Int) (sku : String) (amount : Int) :

The price book after one price change. A sku already in the book keeps its place.

Equations

Lean2Js.Example.repriced prices sku amount = prices.set sku amount

Instances For

Used by

def

Lean2Js.Example.listedSkus

(prices : Dict Int) :

Equations

Lean2Js.Example.listedSkus prices = prices.keys

Instances For

Used by

def

Lean2Js.Example.listedPrices

(prices : Dict Int) :

Equations

Lean2Js.Example.listedPrices prices = prices.values

Instances For

Used by

def

Lean2Js.Example.withdrawn

(prices : Dict Int) (sku : String) :

The price book after a sku is withdrawn. A sku that was never listed leaves the book unchanged.

Equations

Lean2Js.Example.withdrawn prices sku = prices.erase sku

Instances For

Used by

def

Lean2Js.Example.catalogueSize

(prices : Dict Int) :

Equations

Lean2Js.Example.catalogueSize prices = prices.size

Instances For

Used by

The same price book at the other spelling. Dict.Obj crosses the boundary as a plain object rather than as a Map, so JSON.stringify of what these hand back is the book itself. Inside the module the two are one thing, and the operations below are the ones above under different names.

def

Lean2Js.Example.objPriceOf

(prices : Dict.Obj Int) (sku : String) :

Equations

Lean2Js.Example.objPriceOf prices sku = prices.get sku

Instances For

Used by

def

Lean2Js.Example.objIsListed

(prices : Dict.Obj Int) (sku : String) :

Equations

Lean2Js.Example.objIsListed prices sku = prices.has sku

Instances For

Used by

def

Lean2Js.Example.objRepriced

(prices : Dict.Obj Int) (sku : String) (amount : Int) :

The price book after one price change, handed back as an object. A sku already in the book keeps its place.

Equations

Lean2Js.Example.objRepriced prices sku amount = prices.set sku amount

Instances For

Used by

def

Lean2Js.Example.objWithdrawn

(prices : Dict.Obj Int) (sku : String) :

The price book after a sku is withdrawn, handed back as an object.

Equations

Lean2Js.Example.objWithdrawn prices sku = prices.erase sku

Instances For

Used by

def

Lean2Js.Example.objListedSkus

(prices : Dict.Obj Int) :

Equations

Lean2Js.Example.objListedSkus prices = prices.keys

Instances For

Used by

def

Lean2Js.Example.objListedPrices

(prices : Dict.Obj Int) :

Equations

Lean2Js.Example.objListedPrices prices = prices.values

Instances For

Used by

def

Lean2Js.Example.objCatalogueSize

(prices : Dict.Obj Int) :

Equations

Lean2Js.Example.objCatalogueSize prices = prices.size

Instances For

Used by

def

Lean2Js.Example.objLimitsFor

(role : Role) :

What a role may do, written out at the spelling that crosses as a plain object rather than as a Map. Beside limitsFor it is one dictionary written twice: the same entries, the same operations, and what the spelling decides is only what a consumer is handed.

Equations

Lean2Js.Example.objLimitsFor Lean2Js.Example.Role.guest = Lean2Js.Dict.Obj.ofList [("daily", 10), ("monthly", 100)]
Lean2Js.Example.objLimitsFor Lean2Js.Example.Role.member = Lean2Js.Dict.Obj.ofList [("daily", 100), ("monthly", 3000)]
Lean2Js.Example.objLimitsFor Lean2Js.Example.Role.admin = Lean2Js.Dict.Obj.ofList [("daily", 1000), ("monthly", 30000)]

Instances For

Used by

def

Lean2Js.Example.divide

(a b : Int) :

Truncating division. Division by zero traps on the JS side too.

Equations

Lean2Js.Example.divide a b = Lean2Js.Int53.div a b

Instances For

Used by

def

Lean2Js.Example.remainder

(a b : Int) :

Equations

Lean2Js.Example.remainder a b = Lean2Js.Int53.mod a b

Instances For

Used by

def

Lean2Js.Example.taxOn

(amount rate : Int) :

The tax on an amount in minor units at a rate in basis points, rounded half away from zero — which is the rounding an amount of money gets where nothing says otherwise.

Equations

Lean2Js.Example.taxOn amount rate = Lean2Js.Int53.divRound (amount * rate) 10000

Instances For

Used by

def

Lean2Js.Example.shareOf

(cost parties : Int) :

What each of parties carries of a cost, rounded up. A count of zero or less is read as one, since a cost carried by nobody is carried by the one who has it.

Equations

Lean2Js.Example.shareOf cost parties = Lean2Js.Int53.divCeil cost (max parties 1)

Instances For

Used by

def

Lean2Js.Example.evenShare

(amount parties : Int) :

One party's share of an amount split evenly, rounded to the nearest whole unit with a half going away from zero. A count of zero or less is read as one, as shareOf reads it.

Equations

Lean2Js.Example.evenShare amount parties = Lean2Js.Int53.divRound amount (max parties 1)

Instances For

Used by

def

Lean2Js.Example.dayOfInstant

(ms : Int) :

Which whole day an instant falls in, counting from the epoch, where an instant before it belongs to the day it is inside rather than to the one after: divFloor and not div.

Equations

Lean2Js.Example.dayOfInstant ms = Lean2Js.Cal.dayOfInstant ms

Instances For

Used by

def

Lean2Js.Example.dayNumber

(year month day : Int) :

The day a calendar date falls on, counting from 1970-01-01.

Equations

Lean2Js.Example.dayNumber year month day = Lean2Js.Cal.fromCivil year month day

Instances For

Used by

def

Lean2Js.Example.yearOf

(days : Int) :

The calendar year a day number falls in.

Equations

Lean2Js.Example.yearOf days = Lean2Js.Cal.year days

Instances For

Used by

def

Lean2Js.Example.monthOf

(days : Int) :

The calendar month a day number falls in, 1 through 12.

Equations

Lean2Js.Example.monthOf days = Lean2Js.Cal.month days

Instances For

Used by

def

Lean2Js.Example.dayOfMonthOf

(days : Int) :

The day of the month a day number falls on, 1 through 31.

Equations

Lean2Js.Example.dayOfMonthOf days = Lean2Js.Cal.day days

Instances For

Used by

def

Lean2Js.Example.weekdayOf

(days : Int) :

The day of the week a day number falls on, 0 for Sunday through 6 for Saturday.

Equations

Lean2Js.Example.weekdayOf days = Lean2Js.Cal.weekday days

Instances For

Used by

def

Lean2Js.Example.monthLength

(year month : Int) :

How many days a calendar month holds, a leap February included.

Equations

Lean2Js.Example.monthLength year month = Lean2Js.Cal.daysInMonth year month

Instances For

Used by

def

Lean2Js.Example.negate

(a : Int) :

Equations

Lean2Js.Example.negate a = -a

Instances For

Used by

def

Lean2Js.Example.priceGap

(a b : Int) :

Equations

Lean2Js.Example.priceGap a b = Lean2Js.Int53.abs (a - b)

Instances For

Used by

def

Lean2Js.Example.discounted

(amount percent : Int) :

The amount after a percent% discount. The remainder is truncated.

Equations

Lean2Js.Example.discounted amount percent = Lean2Js.Int53.div (amount * (100 - if percent < 0 then 0 else if percent > 100 then 100 else percent)) 100

Instances For

Used by

def

Lean2Js.Example.tenPercentOff

(amount : Int) :

Equations

Lean2Js.Example.tenPercentOff amount = amount - Lean2Js.Int53.div amount 10

Instances For

Used by

def

Lean2Js.Example.rebindTwice

(amount : Int) :

Binds the same name twice. ESM runs in strict mode, so emitting const twice would fail at import time.

Equations

Lean2Js.Example.rebindTwice amount = (amount + 1) * 2

Instances For

Used by

def

Lean2Js.Example.noDiscount

(amount : Int) :

Equations

Lean2Js.Example.noDiscount amount = amount

Instances For

Used by

def

Lean2Js.Example.priced

(rule : Int → Int) (amount : Int) :

Charges an amount under a pricing rule the caller picks. Taking a function keeps it off the public API: there is no way to check at the boundary that one handed in from JS is pure.

Equations

Lean2Js.Example.priced rule amount = rule amount

Instances For

Used by

def

Lean2Js.Example.memberPrice

(amount : Int) :

Equations

Lean2Js.Example.memberPrice amount = Lean2Js.Example.priced Lean2Js.Example.tenPercentOff amount

Instances For

Used by

def

Lean2Js.Example.guestPrice

(amount : Int) :

Equations

Lean2Js.Example.guestPrice amount = Lean2Js.Example.priced Lean2Js.Example.noDiscount amount

Instances For

Used by

def

Lean2Js.Example.mixChannels

(a b : UInt32) :

Equations

Lean2Js.Example.mixChannels a b = a * b + (a - b)

Instances For

Used by

def

Lean2Js.Example.bucketOf

(key buckets : UInt32) :

Equations

Lean2Js.Example.bucketOf key buckets = key % buckets

Instances For

Used by

def

Lean2Js.Example.clampChannel

(value lo hi : UInt32) :

A channel value held between a floor and a ceiling.

Equations

Lean2Js.Example.clampChannel value lo hi = min (max value lo) hi

Instances For

Used by

def

Lean2Js.Example.scaleFee

(fee factor : BigInt) :

Equations

Lean2Js.Example.scaleFee fee factor = fee * factor - 1

Instances For

Used by

def

Lean2Js.Example.bigQuotient

(a b : BigInt) :

Equations

Lean2Js.Example.bigQuotient a b = a.div b

Instances For

Used by

def

Lean2Js.Example.sameLabel

(a b : String) :

Equations

Lean2Js.Example.sameLabel a b = (a == b)

Instances For

Used by

def

Lean2Js.Example.safeQuotientIsPositive

(a b : Int) :

Doubles as a check on short-circuiting. When b is 0 the right-hand side is not evaluated.

Equations

Lean2Js.Example.safeQuotientIsPositive a b = (b != 0 && decide (Lean2Js.Int53.div a b > 0))

Instances For

Used by

def

Lean2Js.Example.canCheckout

(signedIn : Bool) (cartTotal stock : Int) :

Equations

Lean2Js.Example.canCheckout signedIn cartTotal stock = (signedIn && decide (cartTotal > 0) && decide (stock ≥ 1))

Instances For

Used by

def

Lean2Js.Example.cappedCharge

(amount budget : Int) :

Equations

Lean2Js.Example.cappedCharge amount budget = min amount budget

Instances For

Used by

def

Lean2Js.Example.atLeast

(amount floor : Int) :

Equations

Lean2Js.Example.atLeast amount floor = max amount floor

Instances For

Used by

structure

Lean2Js.Example.Money

:

The constructor is named so that the subset reads it as Money; Lean's default mk would make the generated object's tag mk.

constructor Money

amount : Int
currency : String

Instances For

Used by

instance

Lean2Js.Example.instDecidableEqMoney

@[instance_reducible]

:

DecidableEq Money

Equations

Lean2Js.Example.instDecidableEqMoney = Lean2Js.Example.instDecidableEqMoney.decEq

Used by

def

Lean2Js.Example.instDecidableEqMoney.decEq

(x✝ x✝¹ : Money) :

Decidable (x✝ = x✝¹)

Equations

Lean2Js.Example.instDecidableEqMoney.decEq { amount := a, currency := a_1 } { amount := b, currency := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

Instances For

Used by

theorem

Lean2Js.Example.Money.toValue_eq

@[simp]

:

Enc.toValue = toValue

Used by

def

Lean2Js.Example.Money.typeDef

:

Equations

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

Instances For

Used by

def

Lean2Js.Example.Money.ofValue

(v : Value) :

Option Example.Money

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.Money.ofValue v = none

Instances For

Used by

instance

Lean2Js.Example.instEncMoney

@[instance_reducible]

:

Equations

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

Used by

theorem

Lean2Js.Example.Money.ofValue_toValue

(x : Example.Money) :

ofValue x.toValue = some x

Used by

def

Lean2Js.Example.Money.toValue

(x : Example.Money) :

Equations

{ amount := x0, currency := x1 }.toValue = Lean2Js.Value.obj "Money" [("amount", Lean2Js.Enc.toValue x0), ("currency", Lean2Js.Enc.toValue x1)]

Instances For

Used by

def

Lean2Js.Example.Money.accepts

(p : Core.Program) (x : Example.Money) :

Equations

Lean2Js.Example.Money.accepts p { amount := x0, currency := x1 } = (p.findType? "Money" = some Lean2Js.Example.Money.typeDef ∧ Lean2Js.Enc.accepts p x0 ∧ Lean2Js.Enc.accepts p x1)

Instances For

Used by

theorem

Lean2Js.Example.Money.toValue_hasTy

{p : Core.Program} {x : Example.Money} :

accepts p x → Value.hasTy p x.toValue (Core.Ty.named "Money" []) = true

Used by

theorem

Lean2Js.Example.Money.ty_eq

@[simp]

:

Enc.ty Example.Money = Core.Ty.named "Money" []

Used by

inductive

Lean2Js.Example.OrderState

:

Told apart by kind rather than the default tag: which key reads well is the author's call, and the mark above the type is where it is made. The rest of the types here keep tag, so the generated package carries both.

draft : OrderState
placed : OrderState
shipped : OrderState
cancelled : OrderState

Instances For

Used by

instance

Lean2Js.Example.instInhabitedOrderState

@[instance_reducible]

:

Inhabited OrderState

Equations

Lean2Js.Example.instInhabitedOrderState = { default := Lean2Js.Example.instInhabitedOrderState.default }

Used by

theorem

Lean2Js.Example.OrderState.ofValue_toValue

(x : OrderState) :

ofValue x.toValue = some x

Used by

def

Lean2Js.Example.OrderState.ofValue

(v : Value) :

Option OrderState

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.OrderState.ofValue (Lean2Js.Value.obj "draft" []) = some Lean2Js.Example.OrderState.draft
Lean2Js.Example.OrderState.ofValue (Lean2Js.Value.obj "placed" [("orderId", v0)]) = (Lean2Js.Enc.ofValue v0).bind fun (x0 : Int) => some (Lean2Js.Example.OrderState.placed x0)
Lean2Js.Example.OrderState.ofValue (Lean2Js.Value.obj "cancelled" [("reason", v0)]) = (Lean2Js.Enc.ofValue v0).bind fun (x0 : String) => some (Lean2Js.Example.OrderState.cancelled x0)
Lean2Js.Example.OrderState.ofValue v = none

Instances For

Used by

def

Lean2Js.Example.OrderState.typeDef

:

Equations

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

Instances For

Used by

theorem

Lean2Js.Example.OrderState.toValue_eq

@[simp]

:

Enc.toValue = toValue

Used by

instance

Lean2Js.Example.instEncOrderState

@[instance_reducible]

:

Equations

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

Used by

def

Lean2Js.Example.OrderState.accepts

(p : Core.Program) (x : OrderState) :

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.OrderState.accepts p Lean2Js.Example.OrderState.draft = (p.findType? "OrderState" = some Lean2Js.Example.OrderState.typeDef ∧ True)
Lean2Js.Example.OrderState.accepts p (Lean2Js.Example.OrderState.placed x0) = (p.findType? "OrderState" = some Lean2Js.Example.OrderState.typeDef ∧ Lean2Js.Enc.accepts p x0)
Lean2Js.Example.OrderState.accepts p (Lean2Js.Example.OrderState.cancelled x0) = (p.findType? "OrderState" = some Lean2Js.Example.OrderState.typeDef ∧ Lean2Js.Enc.accepts p x0)

Instances For

Used by

def

Lean2Js.Example.OrderState.toValue

(x : OrderState) :

Equations

Lean2Js.Example.OrderState.draft.toValue = Lean2Js.Value.obj "draft" []
(Lean2Js.Example.OrderState.placed x0).toValue = Lean2Js.Value.obj "placed" [("orderId", Lean2Js.Enc.toValue x0)]
(Lean2Js.Example.OrderState.shipped x0 x1).toValue = Lean2Js.Value.obj "shipped" [("orderId", Lean2Js.Enc.toValue x0), ("trackingId", Lean2Js.Enc.toValue x1)]
(Lean2Js.Example.OrderState.cancelled x0).toValue = Lean2Js.Value.obj "cancelled" [("reason", Lean2Js.Enc.toValue x0)]

Instances For

Used by

theorem

Lean2Js.Example.OrderState.toValue_hasTy

{p : Core.Program} {x : OrderState} :

accepts p x → Value.hasTy p x.toValue (Core.Ty.named "OrderState" []) = true

Used by

theorem

Lean2Js.Example.OrderState.ty_eq

@[simp]

:

Enc.ty OrderState = Core.Ty.named "OrderState" []

Used by

def

Lean2Js.Example.addMoney

(a b : Money) :

Except String Money

Amounts in different currencies cannot be added. === is unusable on the JS side, so a structural equality helper is called.

Equations

Lean2Js.Example.addMoney a b = if (a.currency != b.currency) = true then Except.error "currency mismatch" else Except.ok { amount := a.amount + b.amount, currency := a.currency }

Instances For

Used by

def

Lean2Js.Example.sameMoney

(a b : Money) :

Equations

Lean2Js.Example.sameMoney a b = (a == b)

Instances For

Used by

def

Lean2Js.Example.currenciesOf

(items : List Money) :

Equations

Lean2Js.Example.currenciesOf items = List.map (fun (item : Lean2Js.Example.Money) => item.currency) items

Instances For

Used by

def

Lean2Js.Example.cartTotal

(items : List Money) :

Adds the amounts up whatever currency each carries; addMoney is the operation that refuses to mix them.

Equations

Lean2Js.Example.cartTotal items = List.foldl (fun (subtotal : Int) (item : Lean2Js.Example.Money) => subtotal + item.amount) 0 items

Instances For

Used by

def

Lean2Js.Example.cheapestFirst

(items : List Money) :

The lines of a cart, cheapest first. Lines that cost the same keep the order they came in.

Equations

Lean2Js.Example.cheapestFirst items = Lean2Js.Arr.sortByKey items fun (item : Lean2Js.Example.Money) => item.amount

Instances For

Used by

def

Lean2Js.Example.inLabelOrder

(labels : List String) :

Labels in the order the subset compares strings, which counts code points.

Equations

Lean2Js.Example.inLabelOrder labels = Lean2Js.Arr.sortByKey labels fun (label : String) => label

Instances For

Used by

def

Lean2Js.Example.total

(xs : List Int) :

Equations

Lean2Js.Example.total xs = List.foldl (fun (sum x : Int) => sum + x) 0 xs

Instances For

Used by

def

Lean2Js.Example.trackingOf

(state : OrderState) :

Equations

Instances For

Used by

def

Lean2Js.Example.canRefund

(role : Role) (state : OrderState) :

Equations

Instances For

Used by

def

Lean2Js.Example.firstTracking

(states : List OrderState) :

Equations

Lean2Js.Example.firstTracking states = if (Lean2Js.Arr.length states == 0) = true then none else Lean2Js.Example.trackingOf (Lean2Js.Arr.get states 0)

Instances For

Used by

def

Lean2Js.Example.refundableOnly

(role : Role) (states : List OrderState) :

List OrderState

The orders this role may still refund. The predicate reads role from outside the lambda.

Equations

Lean2Js.Example.refundableOnly role states = List.filter (fun (state : Lean2Js.Example.OrderState) => Lean2Js.Example.canRefund role state) states

Instances For

Used by

def

Lean2Js.Example.ship

(state : OrderState) (trackingId : String) :

Except String OrderState

The state transition to shipped. Rejects states that cannot transition and an empty tracking id.

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.ship Lean2Js.Example.OrderState.draft trackingId = Except.error "a draft order cannot ship"
Lean2Js.Example.ship (Lean2Js.Example.OrderState.shipped x0 x1) trackingId = Except.error "the order has already shipped"
Lean2Js.Example.ship (Lean2Js.Example.OrderState.cancelled x0) trackingId = Except.error "a cancelled order cannot ship"

Instances For

Used by

def

Lean2Js.Example.quantityLabel

(quantity : Int) :

The label shown next to a line item.

Equations

Lean2Js.Example.quantityLabel 0 = "out of stock"
Lean2Js.Example.quantityLabel 1 = "last one"
Lean2Js.Example.quantityLabel quantity = "in stock"

Instances For

Used by

def

Lean2Js.Example.renewalLabel

(autoRenew : Bool) :

Whether a subscription carries on. Both cases are named, so no fallback is needed.

Equations

Lean2Js.Example.renewalLabel true = "renews"
Lean2Js.Example.renewalLabel false = "ends"

Instances For

Used by

def

Lean2Js.Example.chargeable

(amount : Money) :

An amount of zero is free whatever the currency, and an amount carrying no currency cannot be charged at all.

Equations

Lean2Js.Example.chargeable { amount := 0, currency := currency } = false
Lean2Js.Example.chargeable { amount := amount_2, currency := "" } = false
Lean2Js.Example.chargeable { amount := value, currency := currency } = decide (value > 0)

Instances For

Used by

def

Lean2Js.Example.settleMessage

(outcome : Except String OrderState) :

The shipping line shown once a transition has been attempted. A draft or cancelled order has nothing to show, so one arm reaches past ok and leaves the state itself open.

Equations

Lean2Js.Example.settleMessage (Except.ok (Lean2Js.Example.OrderState.shipped orderId trackingId)) = trackingId
Lean2Js.Example.settleMessage (Except.ok (Lean2Js.Example.OrderState.placed orderId)) = "awaiting shipment"
Lean2Js.Example.settleMessage (Except.ok a) = "no update"
Lean2Js.Example.settleMessage (Except.error message) = message

Instances For

Used by

def

Lean2Js.Example.settledOrderId

(outcome : Except String OrderState) :

The order the settlement placed, if it placed one. The wildcard here stands for both the states that are not placed and the error, so the split the certificate makes reaches Except as well.

Equations

Lean2Js.Example.settledOrderId (Except.ok (Lean2Js.Example.OrderState.placed orderId)) = orderId
Lean2Js.Example.settledOrderId outcome = 0

Instances For

Used by

def

Lean2Js.Example.dailyLimit

(role : Role) :

A role with no daily limit recorded may do nothing.

Equations

Lean2Js.Example.dailyLimit role = match (Lean2Js.Example.limitsFor role).get "daily" with | some value => value | none => 0

Instances For

Used by

def

Lean2Js.Example.monthlyLimit

(role : Role) :

The same read with the arms the other way round: an arm that binds, then a wildcard for the rest. The certificate splits the scrutinee to show the binding arm did not fire, which Option needs as much as a type the program declares.

Equations

Lean2Js.Example.monthlyLimit role = match (Lean2Js.Example.limitsFor role).get "monthly" with | some value => value | x => 0

Instances For

Used by

structure

Lean2Js.Example.Paginated

(T : Type) :

One page of results together with how many there are in all. The subset carries the parameter as a Ty.var and a use substitutes what it was applied to, so the name here is the one the generated type reads as.

constructor Paginated

items : List T
total : Int

Instances For

Used by

theorem

Lean2Js.Example.Paginated.toValue_eq

@[simp]

{T : Type} [Enc T] :

Enc.toValue = toValue

Used by

theorem

Lean2Js.Example.Paginated.ofValue_toValue

{T : Type} [Enc T] (x : Example.Paginated T) :

ofValue x.toValue = some x

Used by

def

Lean2Js.Example.Paginated.ofValue

{T : Type} [Enc T] (v : Value) :

Option (Example.Paginated T)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.Paginated.ofValue v = none

Instances For

Used by

def

Lean2Js.Example.Paginated.typeDef

:

Equations

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

Instances For

Used by

instance

Lean2Js.Example.instEncPaginated

@[instance_reducible]

{T : Type} [Enc T] :

Enc (Paginated T)

Equations

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

Used by

theorem

Lean2Js.Example.Paginated.toValue_hasTy

{T : Type} [Enc T] {p : Core.Program} {x : Example.Paginated T} :

accepts p x → Value.hasTy p x.toValue (Core.Ty.named "Paginated" [Enc.ty T]) = true

Used by

theorem

Lean2Js.Example.Paginated.ty_eq

@[simp]

{T : Type} [Enc T] :

Enc.ty (Example.Paginated T) = Core.Ty.named "Paginated" [Enc.ty T]

Used by

def

Lean2Js.Example.Paginated.toValue

{T : Type} [Enc T] (x : Example.Paginated T) :

Equations

{ items := x0, total := x1 }.toValue = Lean2Js.Value.obj "Paginated" [("items", Lean2Js.Enc.toValue x0), ("total", Lean2Js.Enc.toValue x1)]

Instances For

Used by

def

Lean2Js.Example.Paginated.accepts

{T : Type} [Enc T] (p : Core.Program) (x : Example.Paginated T) :

Equations

Lean2Js.Example.Paginated.accepts p { items := x0, total := x1 } = (p.findType? "Paginated" = some Lean2Js.Example.Paginated.typeDef ∧ Lean2Js.Enc.accepts p x0 ∧ Lean2Js.Enc.accepts p x1)

Instances For

Used by

inductive

Lean2Js.Example.Validated

(E A : Type) :

What a check concluded: the value it accepted, or the reasons it refused. E is named by only one of the two constructors, so a valid term cannot be read off for it and every use carries both arguments.

valid : Validated E A
invalid : Validated E A

Instances For

Used by

theorem

Lean2Js.Example.Validated.ofValue_toValue

{E A : Type} [Enc E] [Enc A] (x : Validated E A) :

ofValue x.toValue = some x

Used by

theorem

Lean2Js.Example.Validated.toValue_eq

@[simp]

{E A : Type} [Enc E] [Enc A] :

Enc.toValue = toValue

Used by

def

Lean2Js.Example.Validated.toValue

{E A : Type} [Enc E] [Enc A] (x : Validated E A) :

Equations

(Lean2Js.Example.Validated.valid x0).toValue = Lean2Js.Value.obj "valid" [("value", Lean2Js.Enc.toValue x0)]
(Lean2Js.Example.Validated.invalid x0).toValue = Lean2Js.Value.obj "invalid" [("errors", Lean2Js.Enc.toValue x0)]

Instances For

Used by

def

Lean2Js.Example.Validated.accepts

{E A : Type} [Enc E] [Enc A] (p : Core.Program) (x : Validated E A) :

Equations

Lean2Js.Example.Validated.accepts p (Lean2Js.Example.Validated.valid x0) = (p.findType? "Validated" = some Lean2Js.Example.Validated.typeDef ∧ Lean2Js.Enc.accepts p x0)
Lean2Js.Example.Validated.accepts p (Lean2Js.Example.Validated.invalid x0) = (p.findType? "Validated" = some Lean2Js.Example.Validated.typeDef ∧ Lean2Js.Enc.accepts p x0)

Instances For

Used by

theorem

Lean2Js.Example.Validated.toValue_hasTy

{E A : Type} [Enc E] [Enc A] {p : Core.Program} {x : Validated E A} :

accepts p x → Value.hasTy p x.toValue (Core.Ty.named "Validated" [Enc.ty E, Enc.ty A]) = true

Used by

theorem

Lean2Js.Example.Validated.ty_eq

@[simp]

{E A : Type} [Enc E] [Enc A] :

Enc.ty (Validated E A) = Core.Ty.named "Validated" [Enc.ty E, Enc.ty A]

Used by

instance

Lean2Js.Example.instEncValidated

@[instance_reducible]

{E A : Type} [Enc E] [Enc A] :

Enc (Validated E A)

Equations

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

Used by

def

Lean2Js.Example.Validated.ofValue

{E A : Type} [Enc E] [Enc A] (v : Value) :

Option (Validated E A)

Equations

Lean2Js.Example.Validated.ofValue (Lean2Js.Value.obj "valid" [("value", v0)]) = (Lean2Js.Enc.ofValue v0).bind fun (x0 : A) => some (Lean2Js.Example.Validated.valid x0)
Lean2Js.Example.Validated.ofValue (Lean2Js.Value.obj "invalid" [("errors", v0)]) = (Lean2Js.Enc.ofValue v0).bind fun (x0 : List E) => some (Lean2Js.Example.Validated.invalid x0)
Lean2Js.Example.Validated.ofValue v = none

Instances For

Used by

def

Lean2Js.Example.Validated.typeDef

:

Equations

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

Instances For

Used by

def

Lean2Js.Example.remainingItems

(page : Paginated Money) :

How many results lie beyond the page in hand.

Equations

Lean2Js.Example.remainingItems page = page.total - Lean2Js.Arr.length page.items

Instances For

Used by

def

Lean2Js.Example.firstPage

(amounts : List Int) :

The whole list served as a single page.

Equations

Lean2Js.Example.firstPage amounts = { items := amounts, total := Lean2Js.Arr.length amounts }

Instances For

Used by

def

Lean2Js.Example.validateQuantity

(quantity : Int) :

Validated String Int

Accepts an order quantity or says why it was refused.

Equations

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

Instances For

Used by

def

Lean2Js.Example.validationMessage

(outcome : Validated String Int) :

The line shown once a quantity has been checked.

Equations

Lean2Js.Example.validationMessage (Lean2Js.Example.Validated.valid value) = Lean2Js.Example.quantityLabel value
Lean2Js.Example.validationMessage (Lean2Js.Example.Validated.invalid errors) = if (Lean2Js.Arr.length errors == 0) = true then "refused" else Lean2Js.Arr.get errors 0

Instances For

Used by

def

Lean2Js.Example.amountWithTax

(amount : Int) :

The amount and the tax charged on it, as the two lines they are billed as.

Equations

Lean2Js.Example.amountWithTax amount = [amount, Lean2Js.Int53.div amount 10]

Instances For

Used by

def

Lean2Js.Example.currencyOf

(item : Money) :

Equations

Lean2Js.Example.currencyOf item = item.currency

Instances For

Used by

def

Lean2Js.Example.previewLines

(amounts : List Int) (upTo : Int) :

The lines shown before the fold. A count past the end of the order shows the whole of it, where pageOf would have refused the window.

Equations

Lean2Js.Example.previewLines amounts upTo = Lean2Js.Arr.take amounts upTo

Instances For

Used by

def

Lean2Js.Example.linesBelowFold

(amounts : List Int) (upTo : Int) :

Equations

Lean2Js.Example.linesBelowFold amounts upTo = Lean2Js.Arr.drop amounts upTo

Instances For

Used by

def

Lean2Js.Example.cartIsEmpty

(items : List Money) :

Equations

Lean2Js.Example.cartIsEmpty items = Lean2Js.Arr.isEmpty items

Instances For

Used by

def

Lean2Js.Example.stocksSku

(skus : List String) (sku : String) :

Equations

Lean2Js.Example.stocksSku skus sku = Lean2Js.Arr.contains skus sku

Instances For

Used by

def

Lean2Js.Example.amountsTotal

(amounts : List Int) :

Equations

Lean2Js.Example.amountsTotal amounts = Lean2Js.Arr.sum amounts

Instances For

Used by

def

Lean2Js.Example.spreadsheetCount

(fileNames : List String) :

Equations

Lean2Js.Example.spreadsheetCount fileNames = Lean2Js.Arr.count fileNames Lean2Js.Example.isSpreadsheet

Instances For

Used by

def

Lean2Js.Example.firstAmount

(amounts : List Int) :

Equations

Lean2Js.Example.firstAmount amounts = Lean2Js.Arr.head? amounts

Instances For

Used by

def

Lean2Js.Example.latestEvent

(events : List String) :

Equations

Lean2Js.Example.latestEvent events = Lean2Js.Arr.last? events

Instances For

Used by

def

Lean2Js.Example.allLines

(orders : List (List Int)) :

Every line of every order in one list.

Equations

Lean2Js.Example.allLines orders = Lean2Js.Arr.flatten orders

Instances For

Used by

def

Lean2Js.Example.linesWithTax

(amounts : List Int) :

Equations

Lean2Js.Example.linesWithTax amounts = Lean2Js.Arr.flatMap amounts Lean2Js.Example.amountWithTax

Instances For

Used by

def

Lean2Js.Example.noteIsBlank

(note : String) :

Equations

Lean2Js.Example.noteIsBlank note = Lean2Js.Str.isEmpty (Lean2Js.Str.trim note)

Instances For

Used by

def

Lean2Js.Example.priceOr

(prices : Dict Int) (sku : String) (fallback : Int) :

The listed price, or the fallback where the sku is not in the book.

Equations

Lean2Js.Example.priceOr prices sku fallback = prices.getD sku fallback

Instances For

Used by

def

Lean2Js.Example.byCurrency

(items : List Money) :

One line per currency. Where a currency appears twice the later line is the one kept.

Equations

Lean2Js.Example.byCurrency items = Lean2Js.Dict.ofPairs items Lean2Js.Example.currencyOf

Instances For

Used by

def

Lean2Js.Example.quantityOr

(quantity : Option Int) (fallback : Int) :

Equations

Lean2Js.Example.quantityOr quantity fallback = Lean2Js.Opt.getD quantity fallback

Instances For

Used by

def

Lean2Js.Example.discountedIfAny

(amount : Option Int) :

Equations

Lean2Js.Example.discountedIfAny amount = Lean2Js.Opt.map amount Lean2Js.Example.tenPercentOff

Instances For

Used by

def

Lean2Js.Example.settledOrElse

(outcome : Except String Money) (fallback : Money) :

Equations

Lean2Js.Example.settledOrElse outcome fallback = Lean2Js.Exc.getD outcome fallback

Instances For

Used by

def

Lean2Js.Example.settledCurrency

(outcome : Except String Money) :

Except String String

Equations

Lean2Js.Example.settledCurrency outcome = Lean2Js.Exc.map outcome Lean2Js.Example.currencyOf

Instances For

Used by

def

Lean2Js.Example.loudRefusal

(outcome : Except String Money) :

Except String Money

The refusal upper-cased. What the settlement accepted is handed back untouched.

Equations

Lean2Js.Example.loudRefusal outcome = Lean2Js.Exc.mapError outcome Lean2Js.Str.upper

Instances For

Used by

def

Lean2Js.Example.settledMoney

(outcome : Except String Money) :

Equations

Lean2Js.Example.settledMoney outcome = Lean2Js.Exc.toOption outcome

Instances For

Used by

def

Lean2Js.Example.trackingIds

(states : List OrderState) :

The tracking id of every order that has one, and an empty string for the rest. The match is inside the traversal's own function rather than in a declaration of its own.

Equations

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

Instances For

Used by

def

Lean2Js.Example.refundCount

(amounts : List Int) :

How many of the amounts are refunds, with the test written where the count is.

Equations

Lean2Js.Example.refundCount amounts = Lean2Js.Arr.count amounts fun (amount : Int) => decide (amount < 0)

Instances For

Used by

def

Lean2Js.Example.creditNoteAmount

(amount : Int) :

A charge as it appears on a credit note, where money leaving is written negative.

Equations

Lean2Js.Example.creditNoteAmount amount = -1 * max amount 0

Instances For

Used by

def

Lean2Js.Example.directionLabel

(sign : Int) :

What the sign on a statement line means.

Equations

Lean2Js.Example.directionLabel (-1) = "credit"
Lean2Js.Example.directionLabel 1 = "debit"
Lean2Js.Example.directionLabel sign = "none"

Instances For

Used by

inductive

Lean2Js.Example.Category

:

Where a product sits in the catalogue. A group holds categories, so the type names itself and the generated .d.ts type does too.

leaf : Category
group : Category

Instances For

Used by

theorem

Lean2Js.Example.Category.ty_eq

@[simp]

:

Enc.ty Category = Core.Ty.named "Category" []

Used by

theorem

Lean2Js.Example.Category.toValue_hasTy

{p : Core.Program} (hp : p.findType? "Category" = some typeDef) {x : Category} :

acceptsV p x → Value.hasTy p x.toValue (Core.Ty.named "Category" []) = true

Used by

theorem

Lean2Js.Example.Category.toValues_hasTy

{p : Core.Program} (hp : p.findType? "Category" = some typeDef) {xs✝ : List Category} :

acceptsVs p xs✝ → Value.hasElemTy p (List.map toValue xs✝) (Core.Ty.named "Category" []) = true

Used by

theorem

Lean2Js.Example.Category.toValue_eq

@[simp]

:

Enc.toValue = toValue

Used by

def

Lean2Js.Example.Category.ofValues

:

List Value → Option (List Category)

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.Category.ofValues [] = some []

Instances For

Used by

theorem

Lean2Js.Example.Category.denotes_fold

(p : Core.Program) (env : Env) {β : Type} [Enc β] (f0 : String → β) (f1 : String → List β → β) (b0 b1 : Core.Expr) (htd : p.findType? "Category" = some typeDef) (h0 : ∀ (a0 : String), Denote.Denotes p (("name", Enc.toValue a0) :: env) b0 (f0 a0)) (h1 : ∀ (a0 : String) (a1 : List β), Denote.Denotes p (("name", Enc.toValue a0) :: ("children", Enc.toValue a1) :: env) b1 (f1 a0 a1)) (x : Category) {f : Nat} :

f ≤ defaultFuel → ∀ (v : Value), evalFold p f env "Category" [] (foldAlts b0 b1) x.toValue = Except.ok v → v = Enc.toValue (fold f0 f1 x)

Used by

theorem

Lean2Js.Example.Category.denotes_foldList

(p : Core.Program) (env : Env) {β : Type} [Enc β] (f0 : String → β) (f1 : String → List β → β) (b0 b1 : Core.Expr) (htd : p.findType? "Category" = some typeDef) (h0 : ∀ (a0 : String), Denote.Denotes p (("name", Enc.toValue a0) :: env) b0 (f0 a0)) (h1 : ∀ (a0 : String) (a1 : List β), Denote.Denotes p (("name", Enc.toValue a0) :: ("children", Enc.toValue a1) :: env) b1 (f1 a0 a1)) (xs : List Category) {f : Nat} :

f ≤ defaultFuel → ∀ (v : List Value), evalFoldList p f env "Category" [] (foldAlts b0 b1) (List.map toValue xs) = Except.ok v → v = List.map Enc.toValue (foldList f0 f1 xs)

Used by

theorem

Lean2Js.Example.Category.ofValues_map

(xs✝ : List Category) :

ofValues (List.map toValue xs✝) = some xs✝

Used by

def

Lean2Js.Example.Category.toValue

@[irreducible]

(x : Category) :

Equations

(Lean2Js.Example.Category.leaf x0).toValue = Lean2Js.Value.obj "leaf" [("name", Lean2Js.Enc.toValue x0)]
(Lean2Js.Example.Category.group x0 x1).toValue = Lean2Js.Value.obj "group" [("name", Lean2Js.Enc.toValue x0), ("children", Lean2Js.Value.arr (List.map Lean2Js.Example.Category.toValue x1))]

Instances For

Used by

def

Lean2Js.Example.Category.accepts

(p : Core.Program) (x : Category) :

Equations

Lean2Js.Example.Category.accepts p x = (p.findType? "Category" = some Lean2Js.Example.Category.typeDef ∧ Lean2Js.Example.Category.acceptsV p x)

Instances For

Used by

theorem

Lean2Js.Example.Category.ofValue_toValue

(x : Category) :

ofValue x.toValue = some x

Used by

def

Lean2Js.Example.Category.acceptsV

(p : Core.Program) (x : Category) :

Equations

Lean2Js.Example.Category.acceptsV p (Lean2Js.Example.Category.leaf x0) = Lean2Js.Enc.accepts p x0
Lean2Js.Example.Category.acceptsV p (Lean2Js.Example.Category.group x0 x1) = (Lean2Js.Enc.accepts p x0 ∧ Lean2Js.Example.Category.acceptsVs p x1)

Instances For

Used by

def

Lean2Js.Example.Category.ofValue

(v : Value) :

Option Category

Equations

One or more equations did not get rendered due to their size.
Lean2Js.Example.Category.ofValue (Lean2Js.Value.obj "leaf" [("name", v0)]) = (Lean2Js.Enc.ofValue v0).bind fun (x0 : String) => some (Lean2Js.Example.Category.leaf x0)
Lean2Js.Example.Category.ofValue v = none

Instances For

Used by

def

Lean2Js.Example.Category.acceptsVs

(p : Core.Program) :

List Category → Prop

Equations

Lean2Js.Example.Category.acceptsVs p [] = True
Lean2Js.Example.Category.acceptsVs p (y :: ys) = (Lean2Js.Example.Category.acceptsV p y ∧ Lean2Js.Example.Category.acceptsVs p ys)

Instances For

Used by

def

Lean2Js.Example.Category.fold

{β : Type} (f0 : String → β) (f1 : String → List β → β) (x : Category) :

β

Equations

Lean2Js.Example.Category.fold f0 f1 (Lean2Js.Example.Category.leaf x0) = f0 x0
Lean2Js.Example.Category.fold f0 f1 (Lean2Js.Example.Category.group x0 x1) = f1 x0 (Lean2Js.Example.Category.foldList f0 f1 x1)

Instances For

Used by

def

Lean2Js.Example.Category.typeDef

:

Equations

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

Instances For

Used by

instance

Lean2Js.Example.instEncCategory

@[instance_reducible]

:

Equations

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

Used by

def

Lean2Js.Example.Category.foldAlts

(b0 b1 : Core.Expr) :

Equations

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

Instances For

Used by

def

Lean2Js.Example.Category.foldList

{β : Type} (f0 : String → β) (f1 : String → List β → β) (xs : List Category) :

Equations

Lean2Js.Example.Category.foldList f0 f1 [] = []
Lean2Js.Example.Category.foldList f0 f1 (y :: ys) = Lean2Js.Example.Category.fold f0 f1 y :: Lean2Js.Example.Category.foldList f0 f1 ys

Instances For

Used by

def

Lean2Js.Example.categoryName

(category : Category) :

Equations

Lean2Js.Example.categoryName (Lean2Js.Example.Category.leaf x0) = x0
Lean2Js.Example.categoryName (Lean2Js.Example.Category.group x0 x1) = x0

Instances For

Used by

def

Lean2Js.Example.directChildren

(category : Category) :

How many categories sit directly under this one. What sits under those is a walk, which is what categoryProducts takes.

Equations

Instances For

Used by

def

Lean2Js.Example.categoryProducts

(category : Category) :

How many products the catalogue holds, however deep the groups go. A group answers for everything under it, so this walks the whole tree rather than reading one level of it.

Equations

Lean2Js.Example.categoryProducts category = Lean2Js.Example.Category.fold (fun (x : String) => 1) (fun (x : String) (counts : List Int) => Lean2Js.Arr.sum counts) category

Instances For

Used by

theorem

Lean2Js.Example.priceOf_certificate

(prices : Dict Int) (sku : String) :

Denote.Denotes program (bindParams priceOfDecl.params [Enc.toValue prices, Enc.toValue sku]) priceOfDecl.body (priceOf prices sku)

Used by

theorem

Lean2Js.Example.discounted_certificate

(amount percent : Int) :

Denote.Denotes program (bindParams discountedDecl.params [Enc.toValue amount, Enc.toValue percent]) discountedDecl.body (discounted amount percent)

Used by

theorem

Lean2Js.Example.settledOrElse_certificate

(outcome : Except String Money) (fallback : Money) :

Denote.Denotes program (bindParams settledOrElseDecl.params [Enc.toValue outcome, Enc.toValue fallback]) settledOrElseDecl.body (settledOrElse outcome fallback)

Used by

theorem

Lean2Js.Example.firstTracking_certificate

(states : List OrderState) :

Denote.Denotes program (bindParams firstTrackingDecl.params [Enc.toValue states]) firstTrackingDecl.body (firstTracking states)

Used by

theorem

Lean2Js.Example.objIsListed_certificate

(prices : Dict.Obj Int) (sku : String) :

Denote.Denotes program (bindParams objIsListedDecl.params [Enc.toValue prices, Enc.toValue sku]) objIsListedDecl.body (objIsListed prices sku)

Used by

theorem

Lean2Js.Example.firstPage_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams firstPageDecl.params [Enc.toValue amounts]) firstPageDecl.body (firstPage amounts)

Used by

theorem

Lean2Js.Example.lineTotals_certificate

(unitPrice : Int) (quantities : List Int) :

Denote.Denotes program (bindParams lineTotalsDecl.params [Enc.toValue unitPrice, Enc.toValue quantities]) lineTotalsDecl.body (lineTotals unitPrice quantities)

Used by

theorem

Lean2Js.Example.divide_certificate

(a b : Int) :

Denote.Denotes program (bindParams divideDecl.params [Enc.toValue a, Enc.toValue b]) divideDecl.body (divide a b)

Used by

theorem

Lean2Js.Example.noteIsBlank_certificate

(note : String) :

Denote.Denotes program (bindParams noteIsBlankDecl.params [Enc.toValue note]) noteIsBlankDecl.body (noteIsBlank note)

Used by

theorem

Lean2Js.Example.weekdayOf_certificate

(days : Int) :

Denote.Denotes program (bindParams weekdayOfDecl.params [Enc.toValue days]) weekdayOfDecl.body (weekdayOf days)

Used by

theorem

Lean2Js.Example.objListedSkus_certificate

(prices : Dict.Obj Int) :

Denote.Denotes program (bindParams objListedSkusDecl.params [Enc.toValue prices]) objListedSkusDecl.body (objListedSkus prices)

Used by

theorem

Lean2Js.Example.ship_certificate

(state : OrderState) (trackingId : String) :

Denote.Denotes program (bindParams shipDecl.params [Enc.toValue state, Enc.toValue trackingId]) shipDecl.body (ship state trackingId)

Used by

theorem

Lean2Js.Example.cartTotal_certificate

(items : List Money) :

Denote.Denotes program (bindParams cartTotalDecl.params [Enc.toValue items]) cartTotalDecl.body (cartTotal items)

Used by

theorem

Lean2Js.Example.validationMessage_certificate

(outcome : Validated String Int) :

Denote.Denotes program (bindParams validationMessageDecl.params [Enc.toValue outcome]) validationMessageDecl.body (validationMessage outcome)

Used by

theorem

Lean2Js.Example.monthlyLimit_certificate

(role : Role) :

Denote.Denotes program (bindParams monthlyLimitDecl.params [Enc.toValue role]) monthlyLimitDecl.body (monthlyLimit role)

Used by

theorem

Lean2Js.Example.monthOf_certificate

(days : Int) :

Denote.Denotes program (bindParams monthOfDecl.params [Enc.toValue days]) monthOfDecl.body (monthOf days)

Used by

theorem

Lean2Js.Example.roleRank_certificate

(role : Role) :

Denote.Denotes program (bindParams roleRankDecl.params [Enc.toValue role]) roleRankDecl.body (roleRank role)

Used by

theorem

Lean2Js.Example.safeQuotientIsPositive_certificate

(a b : Int) :

Denote.Denotes program (bindParams safeQuotientIsPositiveDecl.params [Enc.toValue a, Enc.toValue b]) safeQuotientIsPositiveDecl.body (safeQuotientIsPositive a b)

Used by

theorem

Lean2Js.Example.loudRefusal_certificate

(outcome : Except String Money) :

Denote.Denotes program (bindParams loudRefusalDecl.params [Enc.toValue outcome]) loudRefusalDecl.body (loudRefusal outcome)

Used by

theorem

Lean2Js.Example.priceGap_certificate

(a b : Int) :

Denote.Denotes program (bindParams priceGapDecl.params [Enc.toValue a, Enc.toValue b]) priceGapDecl.body (priceGap a b)

Used by

theorem

Lean2Js.Example.objWithdrawn_certificate

(prices : Dict.Obj Int) (sku : String) :

Denote.Denotes program (bindParams objWithdrawnDecl.params [Enc.toValue prices, Enc.toValue sku]) objWithdrawnDecl.body (objWithdrawn prices sku)

Used by

theorem

Lean2Js.Example.guestPrice_certificate

(amount : Int) :

Denote.Denotes program (bindParams guestPriceDecl.params [Enc.toValue amount]) guestPriceDecl.body (guestPrice amount)

Used by

theorem

Lean2Js.Example.settledCurrency_certificate

(outcome : Except String Money) :

Denote.Denotes program (bindParams settledCurrencyDecl.params [Enc.toValue outcome]) settledCurrencyDecl.body (settledCurrency outcome)

Used by

theorem

Lean2Js.Example.evenShare_certificate

(amount parties : Int) :

Denote.Denotes program (bindParams evenShareDecl.params [Enc.toValue amount, Enc.toValue parties]) evenShareDecl.body (evenShare amount parties)

Used by

theorem

Lean2Js.Example.objListedPrices_certificate

(prices : Dict.Obj Int) :

Denote.Denotes program (bindParams objListedPricesDecl.params [Enc.toValue prices]) objListedPricesDecl.body (objListedPrices prices)

Used by

theorem

Lean2Js.Example.firstAmount_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams firstAmountDecl.params [Enc.toValue amounts]) firstAmountDecl.body (firstAmount amounts)

Used by

theorem

Lean2Js.Example.bigQuotient_certificate

(a b : BigInt) :

Denote.Denotes program (bindParams bigQuotientDecl.params [Enc.toValue a, Enc.toValue b]) bigQuotientDecl.body (bigQuotient a b)

Used by

theorem

Lean2Js.Example.cappedCharge_certificate

(amount budget : Int) :

Denote.Denotes program (bindParams cappedChargeDecl.params [Enc.toValue amount, Enc.toValue budget]) cappedChargeDecl.body (cappedCharge amount budget)

Used by

theorem

Lean2Js.Example.spreadsheetCount_certificate

(fileNames : List String) :

Denote.Denotes program (bindParams spreadsheetCountDecl.params [Enc.toValue fileNames]) spreadsheetCountDecl.body (spreadsheetCount fileNames)

Used by

theorem

Lean2Js.Example.sameLabel_certificate

(a b : String) :

Denote.Denotes program (bindParams sameLabelDecl.params [Enc.toValue a, Enc.toValue b]) sameLabelDecl.body (sameLabel a b)

Used by

theorem

Lean2Js.Example.yearOf_certificate

(days : Int) :

Denote.Denotes program (bindParams yearOfDecl.params [Enc.toValue days]) yearOfDecl.body (yearOf days)

Used by

theorem

Lean2Js.Example.trackingOf_certificate

(state : OrderState) :

Denote.Denotes program (bindParams trackingOfDecl.params [Enc.toValue state]) trackingOfDecl.body (trackingOf state)

Used by

theorem

Lean2Js.Example.add_certificate

(a b : Int) :

Denote.Denotes program (bindParams addDecl.params [Enc.toValue a, Enc.toValue b]) addDecl.body (add a b)

Used by

theorem

Lean2Js.Example.trackingIds_certificate

(states : List OrderState) :

Denote.Denotes program (bindParams trackingIdsDecl.params [Enc.toValue states]) trackingIdsDecl.body (trackingIds states)

Used by

theorem

Lean2Js.Example.canCheckout_certificate

(signedIn : Bool) (cartTotal stock : Int) :

Denote.Denotes program (bindParams canCheckoutDecl.params [Enc.toValue signedIn, Enc.toValue cartTotal, Enc.toValue stock]) canCheckoutDecl.body (canCheckout signedIn cartTotal stock)

Used by

theorem

Lean2Js.Example.mentionsTerm_certificate

(text term : String) :

Denote.Denotes program (bindParams mentionsTermDecl.params [Enc.toValue text, Enc.toValue term]) mentionsTermDecl.body (mentionsTerm text term)

Used by

theorem

Lean2Js.Example.categoryName_certificate

(category : Category) :

Denote.Denotes program (bindParams categoryNameDecl.params [Enc.toValue category]) categoryNameDecl.body (categoryName category)

Used by

theorem

Lean2Js.Example.amountOr_certificate

(field : String) (fallback : Int) :

Denote.Denotes program (bindParams amountOrDecl.params [Enc.toValue field, Enc.toValue fallback]) amountOrDecl.body (amountOr field fallback)

Used by

theorem

Lean2Js.Example.total_certificate

(xs : List Int) :

Denote.Denotes program (bindParams totalDecl.params [Enc.toValue xs]) totalDecl.body (total xs)

Used by

theorem

Lean2Js.Example.joinFields_certificate

(fields : List String) (separator : String) :

Denote.Denotes program (bindParams joinFieldsDecl.params [Enc.toValue fields, Enc.toValue separator]) joinFieldsDecl.body (joinFields fields separator)

Used by

theorem

Lean2Js.Example.listedSkus_certificate

(prices : Dict Int) :

Denote.Denotes program (bindParams listedSkusDecl.params [Enc.toValue prices]) listedSkusDecl.body (listedSkus prices)

Used by

theorem

Lean2Js.Example.headOr_certificate

(xs : List Int) (fallback : Int) :

Denote.Denotes program (bindParams headOrDecl.params [Enc.toValue xs, Enc.toValue fallback]) headOrDecl.body (headOr xs fallback)

Used by

theorem

Lean2Js.Example.discountedIfAny_certificate

(amount : Option Int) :

Denote.Denotes program (bindParams discountedIfAnyDecl.params [Enc.toValue amount]) discountedIfAnyDecl.body (discountedIfAny amount)

Used by

theorem

Lean2Js.Example.separatorAt_certificate

(reference sep : String) :

Denote.Denotes program (bindParams separatorAtDecl.params [Enc.toValue reference, Enc.toValue sep]) separatorAtDecl.body (separatorAt reference sep)

Used by

theorem

Lean2Js.Example.orderReference_certificate

(«prefix» : String) (orderNo : Int) :

Denote.Denotes program (bindParams orderReferenceDecl.params [Enc.toValue «prefix», Enc.toValue orderNo]) orderReferenceDecl.body (orderReference «prefix» orderNo)

Used by

theorem

Lean2Js.Example.settleMessage_certificate

(outcome : Except String OrderState) :

Denote.Denotes program (bindParams settleMessageDecl.params [Enc.toValue outcome]) settleMessageDecl.body (settleMessage outcome)

Used by

theorem

Lean2Js.Example.sameMoney_certificate

(a b : Money) :

Denote.Denotes program (bindParams sameMoneyDecl.params [Enc.toValue a, Enc.toValue b]) sameMoneyDecl.body (sameMoney a b)

Used by

theorem

Lean2Js.Example.catalogueSize_certificate

(prices : Dict Int) :

Denote.Denotes program (bindParams catalogueSizeDecl.params [Enc.toValue prices]) catalogueSizeDecl.body (catalogueSize prices)

Used by

theorem

Lean2Js.Example.addMoney_certificate

(a b : Money) :

Denote.Denotes program (bindParams addMoneyDecl.params [Enc.toValue a, Enc.toValue b]) addMoneyDecl.body (addMoney a b)

Used by

theorem

Lean2Js.Example.slugOf_certificate

(«prefix» name : String) :

Denote.Denotes program (bindParams slugOfDecl.params [Enc.toValue «prefix», Enc.toValue name]) slugOfDecl.body (slugOf «prefix» name)

Used by

def

Lean2Js.Example.program

:

Equations

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

Instances For

Used by

theorem

Lean2Js.Example.negate_certificate

(a : Int) :

Denote.Denotes program (bindParams negateDecl.params [Enc.toValue a]) negateDecl.body (negate a)

Used by

theorem

Lean2Js.Example.truncateLabel_certificate

(label : String) (limit : Int) :

Denote.Denotes program (bindParams truncateLabelDecl.params [Enc.toValue label, Enc.toValue limit]) truncateLabelDecl.body (truncateLabel label limit)

Used by

theorem

Lean2Js.Example.refiled_certificate

(reference oldSep newSep : String) :

Denote.Denotes program (bindParams refiledDecl.params [Enc.toValue reference, Enc.toValue oldSep, Enc.toValue newSep]) refiledDecl.body (refiled reference oldSep newSep)

Used by

theorem

Lean2Js.Example.canRefund_certificate

(role : Role) (state : OrderState) :

Denote.Denotes program (bindParams canRefundDecl.params [Enc.toValue role, Enc.toValue state]) canRefundDecl.body (canRefund role state)

Used by

theorem

Lean2Js.Example.isSpreadsheet_certificate

(fileName : String) :

Denote.Denotes program (bindParams isSpreadsheetDecl.params [Enc.toValue fileName]) isSpreadsheetDecl.body (isSpreadsheet fileName)

Used by

theorem

Lean2Js.Example.amountWithTax_certificate

(amount : Int) :

Denote.Denotes program (bindParams amountWithTaxDecl.params [Enc.toValue amount]) amountWithTaxDecl.body (amountWithTax amount)

Used by

theorem

Lean2Js.Example.referenceFrom_certificate

(parts : List String) :

Denote.Denotes program (bindParams referenceFromDecl.params [Enc.toValue parts]) referenceFromDecl.body (referenceFrom parts)

Used by

theorem

Lean2Js.Example.storedCoupon_certificate

(campaign entered : String) :

Denote.Denotes program (bindParams storedCouponDecl.params [Enc.toValue campaign, Enc.toValue entered]) storedCouponDecl.body (storedCoupon campaign entered)

Used by

theorem

Lean2Js.Example.dayOfInstant_certificate

(ms : Int) :

Denote.Denotes program (bindParams dayOfInstantDecl.params [Enc.toValue ms]) dayOfInstantDecl.body (dayOfInstant ms)

Used by

theorem

Lean2Js.Example.lineTotal_certificate

(unitPrice quantity : Int) :

Denote.Denotes program (bindParams lineTotalDecl.params [Enc.toValue unitPrice, Enc.toValue quantity]) lineTotalDecl.body (lineTotal unitPrice quantity)

Used by

theorem

Lean2Js.Example.byCurrency_certificate

(items : List Money) :

Denote.Denotes program (bindParams byCurrencyDecl.params [Enc.toValue items]) byCurrencyDecl.body (byCurrency items)

Used by

theorem

Lean2Js.Example.noDiscount_certificate

(amount : Int) :

Denote.Denotes program (bindParams noDiscountDecl.params [Enc.toValue amount]) noDiscountDecl.body (noDiscount amount)

Used by

theorem

Lean2Js.Example.remainingItems_certificate

(page : Paginated Money) :

Denote.Denotes program (bindParams remainingItemsDecl.params [Enc.toValue page]) remainingItemsDecl.body (remainingItems page)

Used by

theorem

Lean2Js.Example.inLabelOrder_certificate

(labels : List String) :

Denote.Denotes program (bindParams inLabelOrderDecl.params [Enc.toValue labels]) inLabelOrderDecl.body (inLabelOrder labels)

Used by

theorem

Lean2Js.Example.tenPercentOff_certificate

(amount : Int) :

Denote.Denotes program (bindParams tenPercentOffDecl.params [Enc.toValue amount]) tenPercentOffDecl.body (tenPercentOff amount)

Used by

theorem

Lean2Js.Example.linesBelowFold_certificate

(amounts : List Int) (upTo : Int) :

Denote.Denotes program (bindParams linesBelowFoldDecl.params [Enc.toValue amounts, Enc.toValue upTo]) linesBelowFoldDecl.body (linesBelowFold amounts upTo)

Used by

theorem

Lean2Js.Example.objPriceOf_certificate

(prices : Dict.Obj Int) (sku : String) :

Denote.Denotes program (bindParams objPriceOfDecl.params [Enc.toValue prices, Enc.toValue sku]) objPriceOfDecl.body (objPriceOf prices sku)

Used by

theorem

Lean2Js.Example.pageOf_certificate

(xs : List Int) (lo hi : Int) :

Denote.Denotes program (bindParams pageOfDecl.params [Enc.toValue xs, Enc.toValue lo, Enc.toValue hi]) pageOfDecl.body (pageOf xs lo hi)

Used by

theorem

Lean2Js.Example.quantityOr_certificate

(quantity : Option Int) (fallback : Int) :

Denote.Denotes program (bindParams quantityOrDecl.params [Enc.toValue quantity, Enc.toValue fallback]) quantityOrDecl.body (quantityOr quantity fallback)

Used by

theorem

Lean2Js.Example.lineNumbers_certificate

(rows : Int) :

Denote.Denotes program (bindParams lineNumbersDecl.params [Enc.toValue rows]) lineNumbersDecl.body (lineNumbers rows)

Used by

theorem

Lean2Js.Example.settledOrderId_certificate

(outcome : Except String OrderState) :

Denote.Denotes program (bindParams settledOrderIdDecl.params [Enc.toValue outcome]) settledOrderIdDecl.body (settledOrderId outcome)

Used by

theorem

Lean2Js.Example.atLeast_certificate

(amount floor : Int) :

Denote.Denotes program (bindParams atLeastDecl.params [Enc.toValue amount, Enc.toValue floor]) atLeastDecl.body (atLeast amount floor)

Used by

theorem

Lean2Js.Example.dayNumber_certificate

(year month day : Int) :

Denote.Denotes program (bindParams dayNumberDecl.params [Enc.toValue year, Enc.toValue month, Enc.toValue day]) dayNumberDecl.body (dayNumber year month day)

Used by

theorem

Lean2Js.Example.amountOf_certificate

(field : String) :

Denote.Denotes program (bindParams amountOfDecl.params [Enc.toValue field]) amountOfDecl.body (amountOf field)

Used by

theorem

Lean2Js.Example.validateQuantity_certificate

(quantity : Int) :

Denote.Denotes program (bindParams validateQuantityDecl.params [Enc.toValue quantity]) validateQuantityDecl.body (validateQuantity quantity)

Used by

theorem

Lean2Js.Example.chargeable_certificate

(amount : Money) :

Denote.Denotes program (bindParams chargeableDecl.params [Enc.toValue amount]) chargeableDecl.body (chargeable amount)

Used by

theorem

Lean2Js.Example.dayOfMonthOf_certificate

(days : Int) :

Denote.Denotes program (bindParams dayOfMonthOfDecl.params [Enc.toValue days]) dayOfMonthOfDecl.body (dayOfMonthOf days)

Used by

theorem

Lean2Js.Example.limitsFor_certificate

(role : Role) :

Denote.Denotes program (bindParams limitsForDecl.params [Enc.toValue role]) limitsForDecl.body (limitsFor role)

Used by

theorem

Lean2Js.Example.remainder_certificate

(a b : Int) :

Denote.Denotes program (bindParams remainderDecl.params [Enc.toValue a, Enc.toValue b]) remainderDecl.body (remainder a b)

Used by

theorem

Lean2Js.Example.monthLength_certificate

(year month : Int) :

Denote.Denotes program (bindParams monthLengthDecl.params [Enc.toValue year, Enc.toValue month]) monthLengthDecl.body (monthLength year month)

Used by

theorem

Lean2Js.Example.repriced_certificate

(prices : Dict Int) (sku : String) (amount : Int) :

Denote.Denotes program (bindParams repricedDecl.params [Enc.toValue prices, Enc.toValue sku, Enc.toValue amount]) repricedDecl.body (repriced prices sku amount)

Used by

theorem

Lean2Js.Example.scaleFee_certificate

(fee factor : BigInt) :

Denote.Denotes program (bindParams scaleFeeDecl.params [Enc.toValue fee, Enc.toValue factor]) scaleFeeDecl.body (scaleFee fee factor)

Used by

theorem

Lean2Js.Example.sortsBefore_certificate

(a b : String) :

Denote.Denotes program (bindParams sortsBeforeDecl.params [Enc.toValue a, Enc.toValue b]) sortsBeforeDecl.body (sortsBefore a b)

Used by

theorem

Lean2Js.Example.bucketOf_certificate

(key buckets : UInt32) :

Denote.Denotes program (bindParams bucketOfDecl.params [Enc.toValue key, Enc.toValue buckets]) bucketOfDecl.body (bucketOf key buckets)

Used by

theorem

Lean2Js.Example.clampChannel_certificate

(value lo hi : UInt32) :

Denote.Denotes program (bindParams clampChannelDecl.params [Enc.toValue value, Enc.toValue lo, Enc.toValue hi]) clampChannelDecl.body (clampChannel value lo hi)

Used by

theorem

Lean2Js.Example.currencyOf_certificate

(item : Money) :

Denote.Denotes program (bindParams currencyOfDecl.params [Enc.toValue item]) currencyOfDecl.body (currencyOf item)

Used by

theorem

Lean2Js.Example.refundableOnly_certificate

(role : Role) (states : List OrderState) :

Denote.Denotes program (bindParams refundableOnlyDecl.params [Enc.toValue role, Enc.toValue states]) refundableOnlyDecl.body (refundableOnly role states)

Used by

theorem

Lean2Js.Example.isListed_certificate

(prices : Dict Int) (sku : String) :

Denote.Denotes program (bindParams isListedDecl.params [Enc.toValue prices, Enc.toValue sku]) isListedDecl.body (isListed prices sku)

Used by

theorem

Lean2Js.Example.priceOr_certificate

(prices : Dict Int) (sku : String) (fallback : Int) :

Denote.Denotes program (bindParams priceOrDecl.params [Enc.toValue prices, Enc.toValue sku, Enc.toValue fallback]) priceOrDecl.body (priceOr prices sku fallback)

Used by

theorem

Lean2Js.Example.referencePrefix_certificate

(reference : String) :

Denote.Denotes program (bindParams referencePrefixDecl.params [Enc.toValue reference]) referencePrefixDecl.body (referencePrefix reference)

Used by

theorem

Lean2Js.Example.settledMoney_certificate

(outcome : Except String Money) :

Denote.Denotes program (bindParams settledMoneyDecl.params [Enc.toValue outcome]) settledMoneyDecl.body (settledMoney outcome)

Used by

theorem

Lean2Js.Example.comparable_certificate

(s : String) :

Denote.Denotes program (bindParams comparableDecl.params [Enc.toValue s]) comparableDecl.body (comparable s)

Used by

theorem

Lean2Js.Example.cheapestFirst_certificate

(items : List Money) :

Denote.Denotes program (bindParams cheapestFirstDecl.params [Enc.toValue items]) cheapestFirstDecl.body (cheapestFirst items)

Used by

theorem

Lean2Js.Example.objRepriced_certificate

(prices : Dict.Obj Int) (sku : String) (amount : Int) :

Denote.Denotes program (bindParams objRepricedDecl.params [Enc.toValue prices, Enc.toValue sku, Enc.toValue amount]) objRepricedDecl.body (objRepriced prices sku amount)

Used by

theorem

Lean2Js.Example.currenciesOf_certificate

(items : List Money) :

Denote.Denotes program (bindParams currenciesOfDecl.params [Enc.toValue items]) currenciesOfDecl.body (currenciesOf items)

Used by

theorem

Lean2Js.Example.combinedCart_certificate

(saved added : List Int) :

Denote.Denotes program (bindParams combinedCartDecl.params [Enc.toValue saved, Enc.toValue added]) combinedCartDecl.body (combinedCart saved added)

Used by

theorem

Lean2Js.Example.directionLabel_certificate

(sign : Int) :

Denote.Denotes program (bindParams directionLabelDecl.params [Enc.toValue sign]) directionLabelDecl.body (directionLabel sign)

Used by

theorem

Lean2Js.Example.categoryProducts_certificate

(category : Category) :

Denote.Denotes program (bindParams categoryProductsDecl.params [Enc.toValue category]) categoryProductsDecl.body (categoryProducts category)

Used by

theorem

Lean2Js.Example.someLineIsFree_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams someLineIsFreeDecl.params [Enc.toValue amounts]) someLineIsFreeDecl.body (someLineIsFree amounts)

Used by

theorem

Lean2Js.Example.couponApplies_certificate

(code campaign : String) :

Denote.Denotes program (bindParams couponAppliesDecl.params [Enc.toValue code, Enc.toValue campaign]) couponAppliesDecl.body (couponApplies code campaign)

Used by

theorem

Lean2Js.Example.directChildren_certificate

(category : Category) :

Denote.Denotes program (bindParams directChildrenDecl.params [Enc.toValue category]) directChildrenDecl.body (directChildren category)

Used by

theorem

Lean2Js.Example.anyOverLimit_certificate

(amounts : List Int) (limit : Int) :

Denote.Denotes program (bindParams anyOverLimitDecl.params [Enc.toValue amounts, Enc.toValue limit]) anyOverLimitDecl.body (anyOverLimit amounts limit)

Used by

theorem

Lean2Js.Example.allLines_certificate

(orders : List (List Int)) :

Denote.Denotes program (bindParams allLinesDecl.params [Enc.toValue orders]) allLinesDecl.body (allLines orders)

Used by

theorem

Lean2Js.Example.amountsTotal_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams amountsTotalDecl.params [Enc.toValue amounts]) amountsTotalDecl.body (amountsTotal amounts)

Used by

theorem

Lean2Js.Example.stocksSku_certificate

(skus : List String) (sku : String) :

Denote.Denotes program (bindParams stocksSkuDecl.params [Enc.toValue skus, Enc.toValue sku]) stocksSkuDecl.body (stocksSku skus sku)

Used by

theorem

Lean2Js.Example.everyLineWithinLimit_certificate

(amounts : List Int) (limit : Int) :

Denote.Denotes program (bindParams everyLineWithinLimitDecl.params [Enc.toValue amounts, Enc.toValue limit]) everyLineWithinLimitDecl.body (everyLineWithinLimit amounts limit)

Used by

theorem

Lean2Js.Example.listedPrices_certificate

(prices : Dict Int) :

Denote.Denotes program (bindParams listedPricesDecl.params [Enc.toValue prices]) listedPricesDecl.body (listedPrices prices)

Used by

theorem

Lean2Js.Example.firstOverLimit_certificate

(amounts : List Int) (limit : Int) :

Denote.Denotes program (bindParams firstOverLimitDecl.params [Enc.toValue amounts, Enc.toValue limit]) firstOverLimitDecl.body (firstOverLimit amounts limit)

Used by

theorem

Lean2Js.Example.cartIsEmpty_certificate

(items : List Money) :

Denote.Denotes program (bindParams cartIsEmptyDecl.params [Enc.toValue items]) cartIsEmptyDecl.body (cartIsEmpty items)

Used by

theorem

Lean2Js.Example.mostRecentFirst_certificate

(events : List String) :

Denote.Denotes program (bindParams mostRecentFirstDecl.params [Enc.toValue events]) mostRecentFirstDecl.body (mostRecentFirst events)

Used by

theorem

Lean2Js.Example.creditNoteAmount_certificate

(amount : Int) :

Denote.Denotes program (bindParams creditNoteAmountDecl.params [Enc.toValue amount]) creditNoteAmountDecl.body (creditNoteAmount amount)

Used by

theorem

Lean2Js.Example.fieldCount_certificate

(row separator : String) :

Denote.Denotes program (bindParams fieldCountDecl.params [Enc.toValue row, Enc.toValue separator]) fieldCountDecl.body (fieldCount row separator)

Used by

theorem

Lean2Js.Example.previewLines_certificate

(amounts : List Int) (upTo : Int) :

Denote.Denotes program (bindParams previewLinesDecl.params [Enc.toValue amounts, Enc.toValue upTo]) previewLinesDecl.body (previewLines amounts upTo)

Used by

theorem

Lean2Js.Example.memberPrice_certificate

(amount : Int) :

Denote.Denotes program (bindParams memberPriceDecl.params [Enc.toValue amount]) memberPriceDecl.body (memberPrice amount)

Used by

theorem

Lean2Js.Example.objCatalogueSize_certificate

(prices : Dict.Obj Int) :

Denote.Denotes program (bindParams objCatalogueSizeDecl.params [Enc.toValue prices]) objCatalogueSizeDecl.body (objCatalogueSize prices)

Used by

theorem

Lean2Js.Example.amountColumn_certificate

(amount : Int) :

Denote.Denotes program (bindParams amountColumnDecl.params [Enc.toValue amount]) amountColumnDecl.body (amountColumn amount)

Used by

theorem

Lean2Js.Example.shareOf_certificate

(cost parties : Int) :

Denote.Denotes program (bindParams shareOfDecl.params [Enc.toValue cost, Enc.toValue parties]) shareOfDecl.body (shareOf cost parties)

Used by

theorem

Lean2Js.Example.priced_certificate

(ruleName : String) (rule : Int → Int) (ruleRuns : Denote.DenotesFn program ruleName rule) (amount : Int) :

Denote.Denotes program (bindParams pricedDecl.params [Value.fn ruleName, Enc.toValue amount]) pricedDecl.body (priced rule amount)

Used by

theorem

Lean2Js.Example.clampQuantity_certificate

(quantity upper : Int) :

Denote.Denotes program (bindParams clampQuantityDecl.params [Enc.toValue quantity, Enc.toValue upper]) clampQuantityDecl.body (clampQuantity quantity upper)

Used by

theorem

Lean2Js.Example.quantityLabel_certificate

(quantity : Int) :

Denote.Denotes program (bindParams quantityLabelDecl.params [Enc.toValue quantity]) quantityLabelDecl.body (quantityLabel quantity)

Used by

theorem

Lean2Js.Example.refundCount_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams refundCountDecl.params [Enc.toValue amounts]) refundCountDecl.body (refundCount amounts)

Used by

theorem

Lean2Js.Example.taxOn_certificate

(amount rate : Int) :

Denote.Denotes program (bindParams taxOnDecl.params [Enc.toValue amount, Enc.toValue rate]) taxOnDecl.body (taxOn amount rate)

Used by

theorem

Lean2Js.Example.latestEvent_certificate

(events : List String) :

Denote.Denotes program (bindParams latestEventDecl.params [Enc.toValue events]) latestEventDecl.body (latestEvent events)

Used by

theorem

Lean2Js.Example.mixChannels_certificate

(a b : UInt32) :

Denote.Denotes program (bindParams mixChannelsDecl.params [Enc.toValue a, Enc.toValue b]) mixChannelsDecl.body (mixChannels a b)

Used by

theorem

Lean2Js.Example.linesWithTax_certificate

(amounts : List Int) :

Denote.Denotes program (bindParams linesWithTaxDecl.params [Enc.toValue amounts]) linesWithTaxDecl.body (linesWithTax amounts)

Used by

theorem

Lean2Js.Example.dailyLimit_certificate

(role : Role) :

Denote.Denotes program (bindParams dailyLimitDecl.params [Enc.toValue role]) dailyLimitDecl.body (dailyLimit role)

Used by

theorem

Lean2Js.Example.rebindTwice_certificate

(amount : Int) :

Denote.Denotes program (bindParams rebindTwiceDecl.params [Enc.toValue amount]) rebindTwiceDecl.body (rebindTwice amount)

Used by

theorem

Lean2Js.Example.objLimitsFor_certificate

(role : Role) :

Denote.Denotes program (bindParams objLimitsForDecl.params [Enc.toValue role]) objLimitsForDecl.body (objLimitsFor role)

Used by

theorem

Lean2Js.Example.renewalLabel_certificate

(autoRenew : Bool) :

Denote.Denotes program (bindParams renewalLabelDecl.params [Enc.toValue autoRenew]) renewalLabelDecl.body (renewalLabel autoRenew)

Used by

theorem

Lean2Js.Example.withdrawn_certificate

(prices : Dict Int) (sku : String) :

Denote.Denotes program (bindParams withdrawnDecl.params [Enc.toValue prices, Enc.toValue sku]) withdrawnDecl.body (withdrawn prices sku)

Used by

theorem

Lean2Js.Example.receiptRule_certificate

(mark : String) :

Denote.Denotes program (bindParams receiptRuleDecl.params [Enc.toValue mark]) receiptRuleDecl.body (receiptRule mark)

Used by

theorem

Lean2Js.Example.add_comm

(a b : Int) :

add a b = add b a

Swapping the arguments of add changes nothing: whatever the two integers, both orders give the same sum.

Used by

theorem

Lean2Js.Example.cheapest_first_keeps_every_line

(items : List Money) :

(cheapestFirst items).Perm items

Ordering a cart by price loses no line and invents none: the answer holds the same lines as the cart it was given, in some order.

Used by

theorem

Lean2Js.Example.monthly_limit_is_not_negative

(role : Role) :

0 ≤ monthlyLimit role

No role's monthly limit is negative, including a role whose book records none.

Used by

theorem

Lean2Js.Example.nothing_under_it_counts_none

(name : String) :

directChildren (Category.leaf name) = 0 ∧ directChildren (Category.group name []) = 0

A category with nothing under it counts nothing under it, whatever it is called. Two shapes have nothing under them — a leaf, and a group holding no categories — and both are here.

Used by

theorem

Lean2Js.Example.a_group_counts_what_is_directly_under_it

(name : String) (children : List Category) :

directChildren (Category.group name children) = Arr.length children

A group counts what sits directly under it, however deep those categories go themselves.

Used by

theorem

Lean2Js.Example.a_leaf_holds_one_product

(name : String) :

categoryProducts (Category.leaf name) = 1

A leaf holds one product, whatever it is called.

Used by

theorem

Lean2Js.Example.an_empty_group_holds_no_product

(name : String) :

categoryProducts (Category.group name []) = 0

A group is not itself a product: a group with nothing under it holds none.

Used by

theorem

Lean2Js.Example.nesting_keeps_the_product

(outer inner first second : String) :

categoryProducts (Category.group outer [Category.group inner [Category.leaf first, Category.leaf second]]) = 2

The walk goes past the first level, which is the whole difference from directChildren: a group whose only child is a group holding two leaves holds both those products, where counting what is directly under it answers one.

Used by

theorem

Lean2Js.Example.a_group_holds_what_its_children_hold

(name : String) (children : List Category) :

categoryProducts (Category.group name children) = Arr.sum (List.map categoryProducts children)

A group holds what its children hold and nothing besides: the count distributes over the children, however deep each of them goes.

Used by

theorem

Lean2Js.Example.failed_settlement_has_no_order_id

(message : String) :

settledOrderId (Except.error message) = 0

A settlement that failed carries no order id, whatever it failed with.

Used by

theorem

Lean2Js.Example.line_total_caps_the_quantity

(unitPrice quantity : Int) (hq : maxLineQuantity < quantity) :

lineTotal unitPrice quantity = unitPrice * maxLineQuantity

A line ordered past the cap is billed at the cap, whatever the unit price.

Used by

theorem

Lean2Js.Example.reference_from_three_parts

(a b c : String) :

referenceFrom [a, b, c] = a ++ "-" ++ b ++ "-" ++ c

Three parts come out of referenceFrom in the order they went in, with a hyphen written between each neighbouring pair. Hyphens the parts themselves carry are not counted, so this says nothing about how many the answer holds.

Used by

theorem

Lean2Js.Example.line_numbers_counts_the_rows

(rows : Int) :

Arr.length (lineNumbers rows) = min (max rows 0) maxReceiptRows

A receipt numbers one row per row it prints: as many numbers as the clamped count says, whatever rows was asked for.

Used by

theorem

Lean2Js.Example.line_numbers_are_rows

(rows k : Int) :

k ∈ lineNumbers rows ↔ 1 ≤ k ∧ k ≤ min (max rows 0) maxReceiptRows

The numbers a receipt prints are exactly the rows it has: a number is one of them when it is at least 1 and at most the clamped count, and is not one of them otherwise.

Used by

def

Lean2Js.Example.money

(amount : Int) (currency : String) :

An amount of money as it crosses the boundary.

Equations

Lean2Js.Example.money amount currency = Lean2Js.Value.obj "Money" [("amount", Lean2Js.Value.int53 amount), ("currency", Lean2Js.Value.str currency)]

Instances For

Used by

theorem

Lean2Js.Example.draft_never_ships

(trackingId : String) :

evalCall program "ship" [Value.obj "draft" [], Value.str trackingId] = Except.ok (Value.obj "error" [("error", Value.str "a draft order cannot ship")])

A draft order cannot ship, whatever tracking id comes with it.

Used by

theorem

Lean2Js.Example.clamped_quantity_in_range

(quantity : Int) (hlo : int53Min ≤ quantity) (hhi : quantity ≤ int53Max) :

∃ (n : Int ), evalCall program "clampQuantity" [Value.int53 quantity, Value.int53 999] = Except.ok (Value.int53 n) ∧ 1 ≤ n ∧ n ≤ 999

Clamping any Int53 quantity to at most 999 lands between 1 and 999.

Used by

theorem

Lean2Js.Example.same_currency_adds

(x y : Int) (currency : String) (hx : int53Min ≤ x ∧ x ≤ int53Max) (hy : int53Min ≤ y ∧ y ≤ int53Max) (hsum : int53Min ≤ x + y ∧ x + y ≤ int53Max) :

evalCall program "addMoney" [money x currency, money y currency] = Except.ok (Value.obj "ok" [("value", money (x + y) currency)])

Two amounts in the same currency add up, as long as their sum stays within Int53.

Used by

The generated function, not just the expression #

Decl.fragment_correct is about a compiled expression. Decl.decl_correct carries it up to a call of the generated function, entry check and all. It holds of every declaration the program has: the fragment covers the whole subset.

The arguments are whatever Decl.ArgsDecode admits, which is the set the entry check lets through and not just the canonical spelling: a JS value whose keys are in another order, or which carries keys the declared type does not name, decodes to the same Value and is covered by the same theorem.

The claims below hold for every reading of the keys the program compiles under, which for this program is the one its types declare: the compiled module and the encoding read one and the same, so the agreement does not depend on which.

theorem

Lean2Js.Example.program_typesNoDictObj

:

program.typesNoDictObj = true

No type this program declares carries a dictionary the declaration told the compiler to hand across the boundary as a plain object rather than as a Map. This is the half encodeAt reads — it recurses into a declared type's fields and never into a declaration — so every claim below whose own return type reaches no such dictionary is stated at encodeValue, the spelling it has always had, through encodeAt_eq_encodeValue.

The program itself does hand one across: objRepriced and objWithdrawn return a Dict.Obj Int, so their entries emit the walk out that Compile.retWalk expands and their results are read at encodeAt rather than at encodeValue. Every other obj declaration takes one and returns something that reaches none, so its entry emits no walk and this theorem carries it to encodeValue like any other.

Used by

theorem

Lean2Js.Example.add_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program addDecl.params jargs args) (he : evalCall program "add" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "add" jargs = Except.ok (encodeValue v)

Whatever arguments the entry check accepts, the generated add returns what eval returns. Its body is a single binary operation.

Used by

theorem

Lean2Js.Example.discounted_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program discountedDecl.params jargs args) (he : evalCall program "discounted" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "discounted" jargs = Except.ok (encodeValue v)

The same for a body that opens with a let, which the compiler emits as a const statement.

Used by

theorem

Lean2Js.Example.rebindTwice_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program rebindTwiceDecl.params jargs args) (he : evalCall program "rebindTwice" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "rebindTwice" jargs = Except.ok (encodeValue v)

And for a body whose second let rebinds a name already in scope, which the compiler leaves as an expression rather than a statement.

Used by

theorem

Lean2Js.Example.memberPrice_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program memberPriceDecl.params jargs args) (he : evalCall program "memberPrice" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "memberPrice" jargs = Except.ok (encodeValue v)

And for a body that calls another declaration, handing it a third by name. The call is where the proof leaves the expression it is looking at: priced applies the function it was given, so the claim about memberPrice rests on the same claim about tenPercentOff.

Used by

Throwing what the reference semantics throws #

Decl.decl_traps is the other half of decl_correct: for arguments the entry accepts, a body that throws is matched by a generated function that throws the same code.

theorem

Lean2Js.Example.program_progOk

:

Cost.progOk program = true

The first of the two checks the emitter runs on a program before it writes anything: every call goes backwards.

Used by

theorem

Lean2Js.Example.program_cost_fits

:

Cost.cost program ≤ defaultFuel

The second: the fuel the artifact runs at covers the deepest call this program can make.

Used by

theorem

Lean2Js.Example.add_traps

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (err : Err) (htyped : ParamsTyped program addDecl.params args) (hdec : Decl.ArgsDecode program addDecl.params jargs args) (he : evalCall program "add" args = Except.error err) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "add" jargs = Except.error err.code

For arguments the entry check decodes to the count and types add declares, whenever eval refuses to return a value the generated function throws the code eval threw. Its body can reach int53Overflow. Running out of fuel is not among the answers: the two checks above rule it out for this program. What falls outside those types never reaches the body at all — that is add_refuses.

Used by

theorem

Lean2Js.Example.add_overflow_throws

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "add" [Js.JsValue.num int53Max, Js.JsValue.num 1] = Except.error "int53Overflow"

The trap is reachable, and reached the same way on both sides: one past the top of Int53 throws int53Overflow out of the generated function.

Used by

theorem

Lean2Js.Example.addMoney_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program addMoneyDecl.params jargs args) (he : evalCall program "addMoney" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "addMoney" jargs = Except.ok (encodeValue v)

The fragment reaches business logic, not just arithmetic: addMoney reads two fields, compares them, and builds a Result around a constructor.

Used by

theorem

Lean2Js.Example.ship_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program shipDecl.params jargs args) (he : evalCall program "ship" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "ship" jargs = Except.ok (encodeValue v)

The fragment reaches a match: ship chooses an arm by the constructor of its scrutinee and reads the fields that arm binds.

Used by

theorem

Lean2Js.Example.cartTotal_calls_agree

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (v : Value) (hdec : Decl.ArgsDecode program cartTotalDecl.params jargs args) (he : evalCall program "cartTotal" args = Except.ok v) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "cartTotal" jargs = Except.ok (encodeValue v)

And an array traversal: cartTotal folds a body over the elements, each under its own binding.

Used by

theorem

Lean2Js.Example.cartTotal_traps

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (err : Err) (htyped : ParamsTyped program cartTotalDecl.params args) (hdec : Decl.ArgsDecode program cartTotalDecl.params jargs args) (he : evalCall program "cartTotal" args = Except.error err) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "cartTotal" jargs = Except.error err.code

The trap side of a traversal: a fold whose running sum leaves Int53 throws where eval does, at the element that overflowed rather than at the end.

Used by

Refusing what the reference semantics refuses #

Decl.decl_refuses needs no InFragment either — the entry check does not look at the body. What it asks for instead is paramsCheckable, which decl_correct does not: a declaration taking another by name has no boundary to check.

theorem

Lean2Js.Example.add_refuses

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (hk : Js.dictKeysDistinctList jargs = true) (hno : ¬Decl.EvalAccepts program addDecl jargs) :

Js.callFunction m "add" jargs = Except.error "typeError"

Whatever add is handed, if no reading of those JS values is a pair of Int53s, the generated function throws instead of computing. The one shape left out is a dictionary holding a key twice, which a Map cannot hold.

Used by

theorem

Lean2Js.Example.add_refuses_string

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) :

Js.callFunction m "add" [Js.JsValue.str "1", Js.JsValue.num 2] = Except.error "typeError"

The hypothesis discharged on a concrete call: a string where an Int53 was declared throws, because no Int53 encodes to one.

Used by

theorem

Lean2Js.Example.addMoney_traps

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jargs : List Js.JsValue) (args : List Value) (err : Err) (htyped : ParamsTyped program addMoneyDecl.params args) (hdec : Decl.ArgsDecode program addMoneyDecl.params jargs args) (he : evalCall program "addMoney" args = Except.error err) :

∃ (g : Nat ), ∀ (g' : Nat), g ≤ g' → Js.callFunctionAt m g' "addMoney" jargs = Except.error err.code

The same for addMoney, under the same declared types: the only way its body throws is the Int53 overflow of the sum, and the generated function throws that code.

Used by

theorem

Lean2Js.Example.file_reads_back

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) :

Parse.parseModule m.render.toList = some m

The text lean2js writes for this program reads back as the module the compiler built. Nothing in between is assumed: the roundtrip holds of whatever compileProgram produces, so the claim carries no side condition about the shape of the module.

Used by

theorem

Lean2Js.Example.helpers_ship_as_modelled

(ext : HelperSem.Ext) (name : String) (args : List Js.JsValue) (r : Js.JsResult) (hok : HelperSem.helperArgsOk name args) (h : Js.helper name args = some r) :

HelperSem.Helper.Calls ext name (List.map HelperSem.ofJs args) (HelperSem.ofRes r)

The runtime helpers are the last hand-written JavaScript in the artifact, and the model of the generated code reaches most of them through one table. Every row of that table is what the source the compiler prints actually computes; helperArgsOk is what a call to a row is still asked for, and it asks only for the Int53 range a type has already given, the distinct keys a Map cannot break, and the shapes on which __eq's walk and the model's structural equality decide the same thing.

__ck and the seven traversal helpers are not rows: the model evaluates them as rules of its own, and HelperProof answers those against the same printed source.

Used by

theorem

Lean2Js.Example.entry_check_fits_dts

(jv : Js.JsValue) (ty : Core.Ty) (b : Nat) (d : Js.TyDesc) (hd : Compile.tyDesc program b ty = Except.ok d) (hc : Js.checkTy [] jv d = true) :

Dts.TsSat program ty jv

Everything the entry check lets through is a value admitted by the type the published .d.ts prints for that parameter. The two are not the same set: the check reads a number's range, which a TypeScript type cannot say, so a call the .d.ts accepts can still be refused at the boundary.

Used by

theorem

Lean2Js.Example.dts_fits_entry_check

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (jv : Js.JsValue) (ty : Core.Ty) (b : Nat) (d : Js.TyDesc) (hd : Compile.tyDesc program b ty = Except.ok d) (hts : Dts.TsSat program ty jv) (hr : Dts.inRange [] jv d = true) :

Js.checkTy [] jv d = true

The other direction, and the one a caller feels: an argument the published .d.ts type admits is one the entry check accepts. Dts.inRange is the whole of what is assumed about the value — the Int53 and UInt32 ranges the check reads, which a TypeScript type cannot express. The order the keys arrive in is not read, and neither are keys the type does not declare.

Used by

theorem

Lean2Js.Example.encoded_values_fit_dts

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (v : Value) (ty : Core.Ty) (hv : Value.hasTy program v ty = true) :

Dts.TsSatOut program ty (encodeAt program ty v)

What comes back, rather than what goes in: a value the reference semantics gives a declared type to, read out through that type, is one the published .d.ts admits at the type it prints for a return, which is the narrower of the two where the type reaches a dictionary crossing as a plain object. typeSound gives the type to whatever a declaration returns, and decl_correct says the generated function returns exactly that reading — so this is the value a consumer meets. Where the type reaches no such dictionary the reading is the encoding itself (encodeAt_eq_encodeValue, program_typesNoDictObj).

Used by

theorem

Lean2Js.Example.returned_values_fit_parameter_types

(ty : Core.Ty) (jv : Js.JsValue) (h : Dts.TsSatOut program ty jv) :

Dts.TsSat program ty jv

The type the .d.ts prints for a return is one the type it prints for a parameter admits, so a call chained onto another type-checks. That is a statement about the two printed types and nothing else; that the value is accepted at run time is returned_values_pass_the_entry_check. This is what lets encoded_values_fit_dts be handed to dts_fits_entry_check.

Used by

theorem

Lean2Js.Example.returned_values_pass_the_entry_check

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (v : Value) (ty : Core.Ty) (b : Nat) (d : Js.TyDesc) (hd : Compile.tyDesc program b ty = Except.ok d) (hv : Value.hasTy program v ty = true) :

Js.checkTy [] (encodeAt program ty v) d = true

And it is accepted, not merely admitted by the type: what one call hands back passes the next call's entry check, with none of the range caveat dts_fits_entry_check carries. The range is what Value.hasTy already says about the value the first call returned, so two exported functions compose with no check of the consumer's own in between. What the second call then computes on is returned_values_read_back_unchanged.

Used by

theorem

Lean2Js.Example.returned_values_read_back_unchanged

[Core.Discriminators] (m : Js.Module) (hm : Compile.compileProgram program = Except.ok m) (v : Value) (ty : Core.Ty) (b : Nat) (d : Js.TyDesc) (hd : Compile.tyDesc program b ty = Except.ok d) (hv : Value.hasTy program v ty = true) :

Js.normTy [] (encodeAt program ty v) d = encodeValue v

The other half of composing two calls: the second entry does not merely accept what the first handed back, it reads it back as the value the first one returned. Together with returned_values_pass_the_entry_check that is the whole of what the crossing costs — what decl_correct says the first call hands back is accepted, and rebuilt as the value it encodes. A dictionary walked out to a plain object becomes the Map the body works in again, and nothing else moves.

Used by

theorem

Lean2Js.Example.steps_agree

(fn : String) (d : Core.Decl) (args : List Value) (hd : program.find? fn = some d) (hpub : d.paramsCheckable = true) :

∃ (n : Nat ), ∀ (bound : Nat), n ≤ bound → stepCall program bound fn args = evalCall program fn args

The small-step machine, given enough steps, answers exactly as eval does every call whose arguments the entry check has a shape to read — which is every exported function, and every internal one that takes no function.

Used by

theorem

Lean2Js.Example.no_rate_is_no_tax

(amount : Int) :

taxOn amount 0 = 0

Nothing is taxed at a rate of zero, whatever the amount.

Used by

theorem

Lean2Js.Example.a_refund_is_taxed_as_the_charge

(amount rate : Int) :

taxOn (-amount) rate = -taxOn amount rate

A refund is taxed exactly as the charge it reverses: the tax on a negative amount is the tax on the positive one, negated. Rounding a half upwards, as JavaScript's Math.round does, would not hold this.

Used by

theorem

Lean2Js.Example.tax_of_five_at_a_tenth

:

taxOn 5 1000 = 1 ∧ taxOn (-5) 1000 = -1

Where the tax lands exactly on a half, it goes away from zero and is not dropped: a tenth of five is one either way round, where truncating would answer zero to both. Two amounts rather than a rule — the symmetry above holds of truncation too, so it is this that says which way a half goes.

Used by

theorem

Lean2Js.Example.the_day_holds_the_instant

(ms : Int) :

dayOfInstant ms * 86400000 ≤ ms ∧ ms < (dayOfInstant ms + 1) * 86400000

The day an instant is filed under is the day that holds it: the instant is at or after that day's first millisecond and before the next day's. It is what says an instant before the epoch belongs to the day it is inside rather than to the one after — truncating division puts the last millisecond before the epoch in day zero, where this rules it out for every instant rather than at one.

Used by

theorem

Lean2Js.Example.shares_cover_the_cost

(cost parties : Int) :

cost ≤ shareOf cost parties * max parties 1

The shares cover the cost: what each of the parties carries, multiplied back out, is never less than the cost itself. Rounding up is what holds it, and it holds however many parties there are, a count of zero or less being read as one.

Used by

def

Lean2Js.Example.manifest

:

Equations

Lean2Js.Example.manifest = { package := "@lean2js/verified-example", version := "0.1.0" }

Instances For

Used by