structure Core.Parse : Type

A grammatical parse represents one reading among potentially many.

• id : String

  Unique identifier for this parse

• description : String

  Human-readable description

def Core.instDecidableEqParse.decEq (x✝ x✝¹ : Parse) : Decidable (x✝ = x✝¹)

Equations

• Core.instDecidableEqParse.decEq { id := a, description := a_1 } { id := b, description := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Core.instDecidableEqParse : DecidableEq Parse

Equations

• Core.instDecidableEqParse = Core.instDecidableEqParse.decEq

def Core.instReprParse.repr : Parse → Nat → Std.Format

Equations

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

instance Core.instReprParse : Repr Parse

Equations

• Core.instReprParse = { reprPrec := Core.instReprParse.repr }

instance Core.instBEqParse : BEq Parse

Equations

• Core.instBEqParse = { beq := Core.instBEqParse.beq }

def Core.instBEqParse.beq : Parse → Parse → Bool

Equations

• Core.instBEqParse.beq { id := a, description := a_1 } { id := b, description := b_1 } = (a == b && a_1 == b_1)
• Core.instBEqParse.beq x✝¹ x✝ = false

instance Core.instHashableParse : Hashable Parse

Equations

• Core.instHashableParse = { hash := Core.instHashableParse.hash }

def Core.instHashableParse.hash : Parse → UInt64

Equations

• Core.instHashableParse.hash { id := a, description := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Core.instToStringParse : ToString Parse

Equations

• Core.instToStringParse = { toString := Core.Parse.id }

def Core.Parse.literal : Parse

The literal/default parse

Equations

• Core.Parse.literal = { id := "lit", description := "Literal/default reading" }

def Core.Parse.surface : Parse

Surface scope parse

Equations

• Core.Parse.surface = { id := "surface", description := "Surface scope (first QP scopes over second)" }

def Core.Parse.inverse : Parse

Inverse scope parse

Equations

• Core.Parse.inverse = { id := "inverse", description := "Inverse scope (second QP scopes over first)" }

def Core.scopeParses : List Parse

Standard scope parses for doubly-quantified sentences

Equations

• Core.scopeParses = [Core.Parse.surface, Core.Parse.inverse]

theorem Core.scope_parses_count : scopeParses.length = 2