inductive Ion.CoreType : Type

• null : CoreType
• bool : CoreType
• int : CoreType
• float : CoreType
• decimal : CoreType
• timestamp : CoreType
• string : CoreType
• symbol : CoreType
• blob : CoreType
• clob : CoreType
• struct : CoreType
• list : CoreType
• sexp : CoreType

@[implicit_reducible]

instance Ion.instBEqCoreType : BEq CoreType

Equations

• Ion.instBEqCoreType = { beq := Ion.instBEqCoreType.beq }

def Ion.instBEqCoreType.beq : CoreType → CoreType → Bool

Equations

• Ion.instBEqCoreType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Ion.instReprCoreType.repr : CoreType → Nat → Std.Format

Equations

• Ion.instReprCoreType.repr Ion.CoreType.null prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.null")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.bool prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.bool")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.int prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.int")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.float prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.float")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.decimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.decimal")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.timestamp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.timestamp")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.string prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.string")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.symbol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.symbol")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.blob prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.blob")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.clob prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.clob")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.struct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.struct")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.list prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.list")).group prec✝
• Ion.instReprCoreType.repr Ion.CoreType.sexp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ion.CoreType.sexp")).group prec✝

@[implicit_reducible]

instance Ion.instReprCoreType : Repr CoreType

Equations

• Ion.instReprCoreType = { reprPrec := Ion.instReprCoreType.repr }

@[implicit_reducible]

instance Ion.instInhabitedCoreType : Inhabited CoreType

Equations

• Ion.instInhabitedCoreType = { default := Ion.instInhabitedCoreType.default }

def Ion.instInhabitedCoreType.default : CoreType

Equations

• Ion.instInhabitedCoreType.default = Ion.CoreType.null

def Ion.CoreType.codes : Array CoreType

Equations

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

inductive Ion.IonF (Sym Ind : Type) : Type

Ion values.

Note. This represents most of the Ion 1.0 values, but is currently missing support for timestamps, blobs, and clob values. Those will be added at a later date.

• null {Sym Ind : Type} (tp : CoreType := CoreType.null) : IonF Sym Ind
• bool {Sym Ind : Type} (b : Bool) : IonF Sym Ind
• int {Sym Ind : Type} (i : Int) : IonF Sym Ind
• float {Sym Ind : Type} (f : Float) : IonF Sym Ind
• decimal {Sym Ind : Type} (d : Decimal) : IonF Sym Ind
• string {Sym Ind : Type} (s : String) : IonF Sym Ind
• symbol {Sym Ind : Type} (s : Sym) : IonF Sym Ind
• blob {Sym Ind : Type} (a : ByteArray) : IonF Sym Ind
• struct {Sym Ind : Type} (a : Array (Sym × Ind)) : IonF Sym Ind
• list {Sym Ind : Type} (a : Array Ind) : IonF Sym Ind
• sexp {Sym Ind : Type} (a : Array Ind) : IonF Sym Ind
• annotation {Sym Ind : Type} (annot : Array Sym) (v : Ind) : IonF Sym Ind

def Ion.instBEqIonF.beq {Sym✝ Ind✝ : Type} [BEq Sym✝] [BEq Ind✝] : IonF Sym✝ Ind✝ → IonF Sym✝ Ind✝ → Bool

Equations

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

@[implicit_reducible]

instance Ion.instBEqIonF {Sym✝ Ind✝ : Type} [BEq Sym✝] [BEq Ind✝] : BEq (IonF Sym✝ Ind✝)

Equations

• Ion.instBEqIonF = { beq := Ion.instBEqIonF.beq }

@[implicit_reducible]

instance Ion.instInhabitedIonF {a✝ a✝¹ : Type} : Inhabited (IonF a✝ a✝¹)

Equations

• Ion.instInhabitedIonF = { default := Ion.instInhabitedIonF.default }

def Ion.instInhabitedIonF.default {a✝ a✝¹ : Type} : IonF a✝ a✝¹

Equations

• Ion.instInhabitedIonF.default = Ion.IonF.null default

def Ion.instReprIonF.repr {Sym✝ Ind✝ : Type} [Repr Sym✝] [Repr Ind✝] : IonF Sym✝ Ind✝ → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Ion.instReprIonF {Sym✝ Ind✝ : Type} [Repr Sym✝] [Repr Ind✝] : Repr (IonF Sym✝ Ind✝)

Equations

• Ion.instReprIonF = { reprPrec := Ion.instReprIonF.repr }

structure Ion.Ion (α : Type) : Type

• app : IonF α (Ion α)

partial def Ion.instReprIon.repr {α✝ : Type} [Repr α✝] : Ion α✝ → Nat → Std.Format

@[implicit_reducible]

instance Ion.instReprIon {α✝ : Type} [Repr α✝] : Repr (Ion α✝)

Equations

• Ion.instReprIon = { reprPrec := Ion.instReprIon.repr }

def Ion.instInhabitedIon.default {a✝ : Type} : Ion a✝

Equations

• Ion.instInhabitedIon.default = { app := default }

@[implicit_reducible]

instance Ion.instInhabitedIon {a✝ : Type} : Inhabited (Ion a✝)

Equations

• Ion.instInhabitedIon = { default := Ion.instInhabitedIon.default }

partial def Ion.instBEqIon.beq {α✝ : Type} [BEq α✝] : Ion α✝ → Ion α✝ → Bool

@[implicit_reducible]

instance Ion.instBEqIon {α✝ : Type} [BEq α✝] : BEq (Ion α✝)

Equations

• Ion.instBEqIon = { beq := Ion.instBEqIon.beq }

def Ion.Ion.null {Sym : Type} (tp : CoreType := CoreType.null) : Ion Sym

Equations

• Ion.Ion.null tp = { app := Ion.IonF.null tp }

def Ion.Ion.bool {Sym : Type} (b : Bool) : Ion Sym

Equations

• Ion.Ion.bool b = { app := Ion.IonF.bool b }

def Ion.Ion.int {Sym : Type} (i : Int) : Ion Sym

Equations

• Ion.Ion.int i = { app := Ion.IonF.int i }

def Ion.Ion.float {Sym : Type} (f : Float) : Ion Sym

Equations

• Ion.Ion.float f = { app := Ion.IonF.float f }

def Ion.Ion.decimal {Sym : Type} (d : Decimal) : Ion Sym

Equations

• Ion.Ion.decimal d = { app := Ion.IonF.decimal d }

def Ion.Ion.string {Sym : Type} (s : String) : Ion Sym

Equations

• Ion.Ion.string s = { app := Ion.IonF.string s }

def Ion.Ion.symbol {Sym : Type} (s : Sym) : Ion Sym

Equations

• Ion.Ion.symbol s = { app := Ion.IonF.symbol s }

def Ion.Ion.blob {Sym : Type} (s : ByteArray) : Ion Sym

Equations

• Ion.Ion.blob s = { app := Ion.IonF.blob s }

def Ion.Ion.struct {Sym : Type} (s : Array (Sym × Ion Sym)) : Ion Sym

Equations

• Ion.Ion.struct s = { app := Ion.IonF.struct s }

def Ion.Ion.list {Sym : Type} (a : Array (Ion Sym)) : Ion Sym

Equations

• Ion.Ion.list a = { app := Ion.IonF.list a }

def Ion.Ion.sexp {Sym : Type} (a : Array (Ion Sym)) : Ion Sym

Equations

• Ion.Ion.sexp a = { app := Ion.IonF.sexp a }

def Ion.Ion.annotation {Sym : Type} (annot : Array Sym) (v : Ion Sym) : Ion Sym

Equations

• Ion.Ion.annotation annot v = { app := Ion.IonF.annotation annot v }

structure Ion.SymbolId : Type

A symbolId denotes an index into an Ion symbol table.

• value : Nat

def Ion.instDecidableEqSymbolId.decEq (x✝ x✝¹ : SymbolId) : Decidable (x✝ = x✝¹)

Equations

• Ion.instDecidableEqSymbolId.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Ion.instDecidableEqSymbolId : DecidableEq SymbolId

Equations

• Ion.instDecidableEqSymbolId = Ion.instDecidableEqSymbolId.decEq

def Ion.instInhabitedSymbolId.default : SymbolId

Equations

• Ion.instInhabitedSymbolId.default = { value := default }

@[implicit_reducible]

instance Ion.instInhabitedSymbolId : Inhabited SymbolId

Equations

• Ion.instInhabitedSymbolId = { default := Ion.instInhabitedSymbolId.default }

@[implicit_reducible]

instance Ion.instReprSymbolId : Repr SymbolId

Equations

• Ion.instReprSymbolId = { reprPrec := Ion.instReprSymbolId.repr }

def Ion.instReprSymbolId.repr : SymbolId → Nat → Std.Format

Equations

• Ion.instReprSymbolId.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

def Ion.SymbolId.zero : SymbolId

Equations

• Ion.SymbolId.zero = { value := 0 }

@[implicit_reducible]

instance Ion.instCoeSymbolIdIon : Coe SymbolId (Ion SymbolId)

Equations

• Ion.instCoeSymbolIdIon = { coe := Ion.instCoeSymbolIdIon._private_1 }