Documentation

Aesop.Forward.PremiseIndex

structure Aesop.PremiseIndex :

toNat : Nat

Instances For

instance Aesop.instInhabitedPremiseIndex :

Inhabited PremiseIndex

Equations

Aesop.instInhabitedPremiseIndex = { default := { toNat := default } }

instance Aesop.instBEqPremiseIndex :

BEq PremiseIndex

Equations

Aesop.instBEqPremiseIndex = { beq := Aesop.beqPremiseIndex✝ }

instance Aesop.instHashablePremiseIndex :

Hashable PremiseIndex

Equations

Aesop.instHashablePremiseIndex = { hash := Aesop.hashPremiseIndex✝ }

instance Aesop.instDecidableEqPremiseIndex :

DecidableEq PremiseIndex

Equations

Aesop.instDecidableEqPremiseIndex = Aesop.decEqPremiseIndex✝

instance Aesop.instOrdPremiseIndex :

Ord PremiseIndex

Equations

Aesop.instOrdPremiseIndex = { compare := Aesop.ordPremiseIndex✝ }

instance Aesop.instLTPremiseIndex :

LT PremiseIndex

Equations

Aesop.instLTPremiseIndex = { lt := fun (i j : Aesop.PremiseIndex) => i.toNat < j.toNat }

instance Aesop.instDecidableRelPremiseIndexLt :

DecidableRel fun (x1 x2 : PremiseIndex) => x1 < x2

Equations

Aesop.instDecidableRelPremiseIndexLt i j = inferInstanceAs (Decidable (i.toNat < j.toNat))

instance Aesop.instLEPremiseIndex :

LE PremiseIndex

Equations

Aesop.instLEPremiseIndex = { le := fun (i j : Aesop.PremiseIndex) => i.toNat ≤ j.toNat }

instance Aesop.instDecidableRelPremiseIndexLe :

DecidableRel fun (x1 x2 : PremiseIndex) => x1 ≤ x2

Equations

Aesop.instDecidableRelPremiseIndexLe i j = inferInstanceAs (Decidable (i.toNat ≤ j.toNat))

instance Aesop.instToStringPremiseIndex :

ToString PremiseIndex

Equations

Aesop.instToStringPremiseIndex = { toString := fun (i : Aesop.PremiseIndex) => toString i.toNat }