inductive RSA.Domains.Quantity.Utterance : Type

Scalar utterances for quantity domains

• none_ : Utterance
• some_ : Utterance
• all : Utterance

def RSA.Domains.Quantity.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

instance RSA.Domains.Quantity.instReprUtterance : Repr Utterance

Equations

• RSA.Domains.Quantity.instReprUtterance = { reprPrec := RSA.Domains.Quantity.instReprUtterance.repr }

instance RSA.Domains.Quantity.instDecidableEqUtterance : DecidableEq Utterance

Equations

• RSA.Domains.Quantity.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.Domains.Quantity.instBEqUtterance : BEq Utterance

Equations

• RSA.Domains.Quantity.instBEqUtterance = { beq := RSA.Domains.Quantity.instBEqUtterance.beq }

def RSA.Domains.Quantity.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• RSA.Domains.Quantity.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def RSA.Domains.Quantity.instInhabitedUtterance.default : Utterance

Equations

• RSA.Domains.Quantity.instInhabitedUtterance.default = RSA.Domains.Quantity.Utterance.none_

instance RSA.Domains.Quantity.instInhabitedUtterance : Inhabited Utterance

Equations

• RSA.Domains.Quantity.instInhabitedUtterance = { default := RSA.Domains.Quantity.instInhabitedUtterance.default }

instance RSA.Domains.Quantity.instFintypeUtterance : Fintype Utterance

Equations

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

def RSA.Domains.Quantity.meaning (n : ℕ) : Utterance → Fin (n + 1) → Bool

Literal semantics (weak "some")

Equations

• RSA.Domains.Quantity.meaning n RSA.Domains.Quantity.Utterance.none_ x✝ = (↑x✝ == 0)
• RSA.Domains.Quantity.meaning n RSA.Domains.Quantity.Utterance.some_ x✝ = decide (↑x✝ ≥ 1)
• RSA.Domains.Quantity.meaning n RSA.Domains.Quantity.Utterance.all x✝ = (↑x✝ == n)

def RSA.Domains.Quantity.allUtterances : List Utterance

All utterances

Equations

• RSA.Domains.Quantity.allUtterances = [RSA.Domains.Quantity.Utterance.none_, RSA.Domains.Quantity.Utterance.some_, RSA.Domains.Quantity.Utterance.all]

def RSA.Domains.Quantity.allWorlds (n : ℕ) : List (Fin (n + 1))

All worlds for a domain of size n

Equations

• RSA.Domains.Quantity.allWorlds n = List.finRange (n + 1)

def RSA.Domains.Quantity.w0 {n : ℕ} : Fin (n + 1)

World where 0 have the property

Equations

• RSA.Domains.Quantity.w0 = ⟨0, ⋯⟩

def RSA.Domains.Quantity.w1 {n : ℕ} (h : 1 < n + 1 := by omega) : Fin (n + 1)

World where 1 has the property

Equations

• RSA.Domains.Quantity.w1 h = ⟨1, h⟩

def RSA.Domains.Quantity.w2 {n : ℕ} (h : 2 < n + 1 := by omega) : Fin (n + 1)

World where 2 have the property

Equations

• RSA.Domains.Quantity.w2 h = ⟨2, h⟩

def RSA.Domains.Quantity.wAll {n : ℕ} : Fin (n + 1)

World where all n have the property

Equations

• RSA.Domains.Quantity.wAll = ⟨n, ⋯⟩

inductive RSA.Domains.Quantity.ExtUtterance : Type

Extended scalar utterances including "most"

• none_ : ExtUtterance
• some_ : ExtUtterance
• most : ExtUtterance
• all : ExtUtterance

def RSA.Domains.Quantity.instReprExtUtterance.repr : ExtUtterance → ℕ → Std.Format

Equations

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

instance RSA.Domains.Quantity.instReprExtUtterance : Repr ExtUtterance

Equations

• RSA.Domains.Quantity.instReprExtUtterance = { reprPrec := RSA.Domains.Quantity.instReprExtUtterance.repr }

instance RSA.Domains.Quantity.instDecidableEqExtUtterance : DecidableEq ExtUtterance

Equations

• RSA.Domains.Quantity.instDecidableEqExtUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.Domains.Quantity.instBEqExtUtterance.beq : ExtUtterance → ExtUtterance → Bool

Equations

• RSA.Domains.Quantity.instBEqExtUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.Domains.Quantity.instBEqExtUtterance : BEq ExtUtterance

Equations

• RSA.Domains.Quantity.instBEqExtUtterance = { beq := RSA.Domains.Quantity.instBEqExtUtterance.beq }

instance RSA.Domains.Quantity.instInhabitedExtUtterance : Inhabited ExtUtterance

Equations

• RSA.Domains.Quantity.instInhabitedExtUtterance = { default := RSA.Domains.Quantity.instInhabitedExtUtterance.default }

def RSA.Domains.Quantity.instInhabitedExtUtterance.default : ExtUtterance

Equations

• RSA.Domains.Quantity.instInhabitedExtUtterance.default = RSA.Domains.Quantity.ExtUtterance.none_

instance RSA.Domains.Quantity.instFintypeExtUtterance : Fintype ExtUtterance

Equations

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

def RSA.Domains.Quantity.extMeaning (n : ℕ) : ExtUtterance → Fin (n + 1) → Bool

Extended semantics with "most"

Equations

• RSA.Domains.Quantity.extMeaning n RSA.Domains.Quantity.ExtUtterance.none_ x✝ = (↑x✝ == 0)
• RSA.Domains.Quantity.extMeaning n RSA.Domains.Quantity.ExtUtterance.some_ x✝ = decide (↑x✝ ≥ 1)
• RSA.Domains.Quantity.extMeaning n RSA.Domains.Quantity.ExtUtterance.most x✝ = decide (↑x✝ * 2 > n)
• RSA.Domains.Quantity.extMeaning n RSA.Domains.Quantity.ExtUtterance.all x✝ = (↑x✝ == n)

def RSA.Domains.Quantity.allExtUtterances : List ExtUtterance

All extended utterances

Equations

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

@[reducible, inline]

abbrev VanTielQuantity.Utterance : Type

Equations

• VanTielQuantity.Utterance = Fragments.English.Determiners.QuantityWord

@[reducible, inline]

abbrev VanTielQuantity.Monotonicity : Type

Equations

• VanTielQuantity.Monotonicity = Fragments.English.Determiners.Monotonicity

def VanTielQuantity.allUtterances : List Utterance

Equations

• VanTielQuantity.allUtterances = Fragments.English.Determiners.QuantityWord.toList

def VanTielQuantity.monotonicity (u : Utterance) : Monotonicity

Get monotonicity from unified entry

Equations

• VanTielQuantity.monotonicity u = Fragments.English.Determiners.QuantityWord.monotonicity u

def VanTielQuantity.gqtMeaning (n : ℕ) (m : Utterance) (t : Fin (n + 1)) : Bool

GQT meaning from unified entry

Equations

• VanTielQuantity.gqtMeaning n m t = Fragments.English.Determiners.QuantityWord.gqtMeaning n m t

def VanTielQuantity.allWorlds (n : ℕ) : List (Fin (n + 1))

Equations

• VanTielQuantity.allWorlds n = List.finRange (n + 1)