inductive ConcreteOrMVar (α : Type u) (φ : ℕ) : Type u

A general type that is either a concrete known value of type α, or one of φ metavariables

• concrete: {α : Type u} → {φ : ℕ} → α → ConcreteOrMVar α φ
• mvar: {α : Type u} → {φ : ℕ} → Fin φ → ConcreteOrMVar α φ

instance instDecidableEqConcreteOrMVar : {α : Type u_1} → {φ : ℕ} → [inst : DecidableEq α] → DecidableEq (ConcreteOrMVar α φ)

Equations

• instDecidableEqConcreteOrMVar = decEqConcreteOrMVar✝

instance instReprConcreteOrMVar : {α : Type u_1} → {φ : ℕ} → [inst : Repr α] → Repr (ConcreteOrMVar α φ)

Equations

• instReprConcreteOrMVar = { reprPrec := reprConcreteOrMVar✝ }

instance instInhabitedConcreteOrMVar : {a : Type u_1} → [inst : Inhabited a] → {a_1 : ℕ} → Inhabited (ConcreteOrMVar a a_1)

Equations

• instInhabitedConcreteOrMVar = { default := ConcreteOrMVar.concrete default }

instance instToStringConcreteOrMVar {α : Type u_1} {n : ℕ} [ToString α] : ToString (ConcreteOrMVar α n)

Equations

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

instance instCoeConcreteOrMVar {α : Type u_1} {φ : ℕ} : Coe α (ConcreteOrMVar α φ)

A coercion from the concrete type α to the ConcreteOrMVar

Equations

• instCoeConcreteOrMVar = { coe := ConcreteOrMVar.concrete }

instance instOfNatConcreteOrMVarNat {φ : ℕ} {n : ℕ} : OfNat (ConcreteOrMVar ℕ φ) n

Equations

• instOfNatConcreteOrMVarNat = { ofNat := ConcreteOrMVar.concrete n }

def ConcreteOrMVar.toConcrete {α : Type u_1} : ConcreteOrMVar α 0 → α

If there are no meta-variables, ConcreteOrMVar is just the concrete type α

Equations

• (ConcreteOrMVar.concrete a).toConcrete = a

@[simp]

theorem ConcreteOrMVar.toConcrete_concrete : ∀ {α : Type u_1} {a : α}, (ConcreteOrMVar.concrete a).toConcrete = a

def ConcreteOrMVar.instantiateOne {α : Type u_1} {φ : ℕ} (a : α) : ConcreteOrMVar α (φ + 1) → ConcreteOrMVar α φ

Provide a value for one of the metavariables. Specifically, the metavariable with the maximal index φ out of φ+1 total metavariables. All other metavariables indices' are left as-is, but cast to Fin φ

Equations

• ConcreteOrMVar.instantiateOne a (ConcreteOrMVar.concrete w) = ConcreteOrMVar.concrete w
• ConcreteOrMVar.instantiateOne a (ConcreteOrMVar.mvar i) = Fin.lastCases (ConcreteOrMVar.concrete a) (fun (j : Fin φ) => ConcreteOrMVar.mvar j) i

def ConcreteOrMVar.instantiate {α : Type u_1} {φ : ℕ} (as : Mathlib.Vector α φ) : ConcreteOrMVar α φ → α

Instantiate all meta-variables

Equations

• ConcreteOrMVar.instantiate as (ConcreteOrMVar.concrete a) = a
• ConcreteOrMVar.instantiate as (ConcreteOrMVar.mvar a) = as.get a

@[simp]

def ConcreteOrMVar.ofNat_eq_concrete {φ : ℕ} (x : ℕ) : OfNat.ofNat x = ConcreteOrMVar.concrete x

We choose ConcreteOrMVar.concrete to be our simp normal form.

Equations

• ⋯ = ⋯

@[simp]

def ConcreteOrMVar.instantiate_ofNat_eq {φ : ℕ} (as : Mathlib.Vector ℕ φ) (x : ℕ) : ConcreteOrMVar.instantiate as (OfNat.ofNat x) = x

Equations

• ⋯ = ⋯

@[simp]

theorem ConcreteOrMVar.instantiate_mvar_zero : ∀ {α : Type u_1} {w : α} {ws : List α} {φ : ℕ} {hφ : (w :: ws).length = φ} {h0 : 0 < φ}, ConcreteOrMVar.instantiate ⟨w :: ws, hφ⟩ (ConcreteOrMVar.mvar ⟨0, h0⟩) = w

@[simp]

theorem ConcreteOrMVar.instantiate_mvar_zero' : ∀ {α : Type u_1} {w : α}, ConcreteOrMVar.instantiate ⟨[w], ⋯⟩ (ConcreteOrMVar.mvar ⟨0, ⋯⟩) = w

@[simp]

theorem ConcreteOrMVar.instantiate_mvar_zero'' : ∀ {α : Type u_1} {w : α} {h1 : [w].length = 1}, ConcreteOrMVar.instantiate ⟨[w], h1⟩ (ConcreteOrMVar.mvar 0) = w