inductive SecondOrder.Kind : Type

• star: SecondOrder.Kind

instance SecondOrder.instReprKind : Repr SecondOrder.Kind

Equations

• SecondOrder.instReprKind = { reprPrec := SecondOrder.reprKind✝ }

instance SecondOrder.instDecidableEqKind : DecidableEq SecondOrder.Kind

Equations

• SecondOrder.instDecidableEqKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

def SecondOrder.«term∗» : Lean.ParserDescr

Equations

• SecondOrder.«term∗» = Lean.ParserDescr.node `SecondOrder.term∗ 1024 (Lean.ParserDescr.symbol " ∗ ")

instance SecondOrder.instToStringKind : ToString SecondOrder.Kind

Equations

• SecondOrder.instToStringKind = { toString := fun (k : SecondOrder.Kind) => match k with | ∗ => "∗" }

inductive SecondOrder.Typ : Type

• var: Name → SecondOrder.Typ
• arrow: SecondOrder.Typ → SecondOrder.Typ → SecondOrder.Typ
• pi: Name → SecondOrder.Kind → SecondOrder.Typ → SecondOrder.Typ

instance SecondOrder.instReprTyp : Repr SecondOrder.Typ

Equations

• SecondOrder.instReprTyp = { reprPrec := SecondOrder.reprTyp✝ }

instance SecondOrder.instDecidableEqTyp : DecidableEq SecondOrder.Typ

Equations

• SecondOrder.instDecidableEqTyp = SecondOrder.decEqTyp✝

def SecondOrder.Typ.toString : SecondOrder.Typ → String

Equations

• (SecondOrder.Typ.var a).toString = a
• (a ⇒ a_1).toString = toString "(" ++ toString a.toString ++ toString " → " ++ toString a_1.toString ++ toString ")"
• (SecondOrder.Typ.pi a a_1 a_2).toString = toString "(Π " ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"

instance SecondOrder.Typ.instToString : ToString SecondOrder.Typ

Equations

• SecondOrder.Typ.instToString = { toString := SecondOrder.Typ.toString }

instance SecondOrder.Typ.instCoeName : Coe Name SecondOrder.Typ

Equations

• SecondOrder.Typ.instCoeName = { coe := SecondOrder.Typ.var }

def SecondOrder.Typ.«term_⇒_» : Lean.TrailingParserDescr

Equations

• SecondOrder.Typ.«term_⇒_» = Lean.ParserDescr.trailingNode `SecondOrder.Typ.term_⇒_ 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 20))

def SecondOrder.Typ.«termΠ_:_↦_» : Lean.ParserDescr

Equations

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

def SecondOrder.Typ.FTV : SecondOrder.Typ → Finset Name

Equations

• (SecondOrder.Typ.var a).FTV = {a}
• (a ⇒ a_1).FTV = a.FTV ∪ a_1.FTV
• (SecondOrder.Typ.pi a a_1 a_2).FTV = a_2.FTV \ {a}

def SecondOrder.Typ.subst (A : SecondOrder.Typ) (α : Name) (B : SecondOrder.Typ) : SecondOrder.Typ

Equations

• (SecondOrder.Typ.var a).subst α B = if α = a then B else SecondOrder.Typ.var a
• (a ⇒ a_1).subst α B = (a.subst α B ⇒ a_1.subst α B)
• (SecondOrder.Typ.pi a a_1 a_2).subst α B = if α = a ∨ a ∈ B.FTV then SecondOrder.Typ.pi a a_1 a_2 else SecondOrder.Typ.pi a a_1 (a_2.subst α B)

def SecondOrder.Typ.«term_[_:=_,_]» : Lean.TrailingParserDescr

Equations

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

inductive SecondOrder.Term : Type

• var: Name → SecondOrder.Term
• app: SecondOrder.Term → SecondOrder.Term → SecondOrder.Term
• tapp: SecondOrder.Term → SecondOrder.Typ → SecondOrder.Term
• abs: Name → SecondOrder.Typ → SecondOrder.Term → SecondOrder.Term
• tabs: Name → SecondOrder.Kind → SecondOrder.Term → SecondOrder.Term

instance SecondOrder.instReprTerm : Repr SecondOrder.Term

Equations

• SecondOrder.instReprTerm = { reprPrec := SecondOrder.reprTerm✝ }

instance SecondOrder.instDecidableEqTerm : DecidableEq SecondOrder.Term

Equations

• SecondOrder.instDecidableEqTerm = SecondOrder.decEqTerm✝

def SecondOrder.Term.toString : SecondOrder.Term → String

Equations

• (SecondOrder.Term.var a).toString = a
• (a ∙ a_1).toString = toString "(" ++ toString a.toString ++ toString " " ++ toString a_1.toString ++ toString ")"
• (a ∙ₜ a_1).toString = toString "(" ++ toString a.toString ++ toString " " ++ toString a_1.toString ++ toString ")"
• (SecondOrder.Term.abs a a_1 a_2).toString = toString "(λ" ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"
• (SecondOrder.Term.tabs a a_1 a_2).toString = toString "(Λ" ++ toString a ++ toString " : " ++ toString a_1 ++ toString ". " ++ toString a_2.toString ++ toString ")"

instance SecondOrder.Term.instToString : ToString SecondOrder.Term

Equations

• SecondOrder.Term.instToString = { toString := SecondOrder.Term.toString }

instance SecondOrder.Term.instCoeName : Coe Name SecondOrder.Term

Equations

• SecondOrder.Term.instCoeName = { coe := SecondOrder.Term.var }

def SecondOrder.Term.«term_∙_» : Lean.TrailingParserDescr

Equations

• SecondOrder.Term.«term_∙_» = Lean.ParserDescr.trailingNode `SecondOrder.Term.term_∙_ 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 101))

def SecondOrder.Term.«term_∙ₜ_» : Lean.TrailingParserDescr

Equations

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

def SecondOrder.Term.«termΛ_:_↦_» : Lean.ParserDescr

Equations

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

def SecondOrder.Term.«termƛ_:_↦_» : Lean.ParserDescr

Equations

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

inductive SecondOrder.Declaration : Type

• type: Name × SecondOrder.Typ → SecondOrder.Declaration
• kind: Name × SecondOrder.Kind → SecondOrder.Declaration

instance SecondOrder.instReprDeclaration : Repr SecondOrder.Declaration

Equations

• SecondOrder.instReprDeclaration = { reprPrec := SecondOrder.reprDeclaration✝ }

instance SecondOrder.instDecidableEqDeclaration : DecidableEq SecondOrder.Declaration

Equations

• SecondOrder.instDecidableEqDeclaration = SecondOrder.decEqDeclaration✝

instance SecondOrder.instCoeProdNameTypDeclaration : Coe (Name × SecondOrder.Typ) SecondOrder.Declaration

Equations

• SecondOrder.instCoeProdNameTypDeclaration = { coe := SecondOrder.Declaration.type }

instance SecondOrder.instCoeProdNameKindDeclaration : Coe (Name × SecondOrder.Kind) SecondOrder.Declaration

Equations

• SecondOrder.instCoeProdNameKindDeclaration = { coe := SecondOrder.Declaration.kind }

@[reducible, inline]

abbrev SecondOrder.Context : Type

Equations

• SecondOrder.Context = Finset SecondOrder.Declaration

inductive SecondOrder.HasKind : SecondOrder.Context → SecondOrder.Typ → SecondOrder.Kind → Prop

• var: ∀ {Γ : SecondOrder.Context} {x : Name}, Γ ⊢ₖ SecondOrder.Typ.var x : ∗
• arrow: ∀ {Γ : SecondOrder.Context} {σ τ : SecondOrder.Typ}, (Γ ⊢ₖ σ : ∗ ) → (Γ ⊢ₖ τ : ∗ ) → Γ ⊢ₖ σ ⇒ τ : ∗

inductive SecondOrder.HasType : SecondOrder.Context → SecondOrder.Term → SecondOrder.Typ → Prop

• var: ∀ {Γ : SecondOrder.Context} {x : Name} {σ : SecondOrder.Typ}, SecondOrder.Declaration.type (x, σ) ∈ Γ → Γ ⊢ SecondOrder.Term.var x : σ
• app: ∀ {Γ : SecondOrder.Context} {M N : SecondOrder.Term} {σ τ : SecondOrder.Typ}, (Γ ⊢ M : σ ⇒ τ) → (Γ ⊢ N : σ) → Γ ⊢ M ∙ N : τ
• abs: ∀ {Γ : SecondOrder.Context} {x : Name} {M : SecondOrder.Term} {σ τ : SecondOrder.Typ}, (insert (SecondOrder.Declaration.type (x, σ)) Γ ⊢ M : τ) → Γ ⊢ SecondOrder.Term.abs x σ M : σ ⇒ τ
• tabs: ∀ {Γ : SecondOrder.Context} {α : Name} {M : SecondOrder.Term} {A : SecondOrder.Typ}, (insert (SecondOrder.Declaration.kind (α, ∗ )) Γ ⊢ M : A) → Γ ⊢ SecondOrder.Term.tabs α ∗ M : SecondOrder.Typ.pi α ∗ A
• tapp: ∀ {Γ : SecondOrder.Context} {α : Name} {M : SecondOrder.Term} {A B : SecondOrder.Typ}, (Γ ⊢ M : SecondOrder.Typ.pi α ∗ A) → (Γ ⊢ₖ B : ∗ ) → Γ ⊢ M ∙ₜ B : A.subst α B

def SecondOrder.«term_⊢_:_» : Lean.TrailingParserDescr

Equations

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

def SecondOrder.«term_⊢ₖ_:_» : Lean.TrailingParserDescr

Equations

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

def SecondOrder.Statement (M : SecondOrder.Term) (σ : SecondOrder.Typ) : Prop

Equations

• (⊢ M : σ) = ∃ (Γ : SecondOrder.Context), Γ ⊢ M : σ

def SecondOrder.KindStatement (σ : SecondOrder.Typ) (k : SecondOrder.Kind) : Prop

Equations

• (⊢ₖ σ : k) = ∃ (Γ : SecondOrder.Context), Γ ⊢ₖ σ : k

def SecondOrder.«term⊢_:_» : Lean.ParserDescr

Equations

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

def SecondOrder.«term⊢ₖ_:_» : Lean.ParserDescr

Equations

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

def SecondOrder.Combinators.id : SecondOrder.Term

Equations

• SecondOrder.Combinators.id = SecondOrder.Term.tabs "α" ∗ (SecondOrder.Term.abs "x" (SecondOrder.Typ.var "α") (SecondOrder.Term.var "x"))

def SecondOrder.Combinators.D : SecondOrder.Term

Equations

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

def SecondOrder.Combinators.compose : SecondOrder.Term

Equations

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