Skip to content

SymbolFact

type SymbolFact =
    {
        Type: string option
        Binders: Map<string,string>
        Assumptions: Assumptions option
    }
Assembly Nacara.Plugin.Rocq

What Rocq reported about a symbol. An absent field means Rocq gave no answer.

Fields

Type: string option

The type as Rocq prints it.

Binders: Map<string,string>

The leading quantifier's binders: name to type, in printed form.

Assumptions: Assumptions option

Present for theorems only.