Cairn.Claims.Elab
lean/Cairn/Claims/Elab.lean
The claim commands: move, flow, invariant, assume, place and retire, and the
moves% and claims% terms. See docs/claims.md for the syntax and what each check
guarantees.
Each command elaborates to ordinary declarations (definitions for the formal statement,
theorems for the evidence, a ClaimInfo and a value of the claim's structure) and records an
Entry in the registry. Every check happens here, at compile time:
- an id is issued once in the whole imported environment;
- every claim has a title and says what it does (
does); a move also says what follows (sees); in ^Pnames a place that exists;- a move has a handler per trigger, and each handler has
apply(oremit),postand asoundproof, so a move without a proof does not compile; - a flow's witness names moves that exist, and its
liveandreachesproofs check; - a retired id says why;
- no move is declared after
moves%collected its namespace, and no claim afterclaims%.
Imports Lean, Cairn.Claims.Core, Cairn.Claims.Registry
Structures 1
Clauses : Type
The clauses of one claim, checked against the names its kind allows.
items : Array Item
Inductive types 1
Item : Type
prose (name : Lean.Syntax) (val : String) : Item
defn (name : Lean.Syntax) (binders : Array Lean.Syntax) (rhs : Lean.Term) : Item
witness (ref : Lean.Syntax) (steps : Array Lean.Syntax) : Item
Definitions 62
claimKw (s : String) : Lean.Parser.Parser
A command keyword that is not reserved.
moveKw : Lean.Parser.Parser
flowKw : Lean.Parser.Parser
invariantKw : Lean.Parser.Parser
assumeKw : Lean.Parser.Parser
placeKw : Lean.Parser.Parser
retireKw : Lean.Parser.Parser
claimRef : Lean.ParserDescrA claim id, ^N.
claimStep : Lean.ParserDescrOne action of a flow's witness: press ^1, press ^5#12, edit ^3 (.insert "a").
claimItem : Lean.ParserDescrA prose clause (does "…") or a definition clause (post s' := …, sound := by …).
claimWitness : Lean.ParserDescr
claimOn : Lean.ParserDescrA move's handler for one trigger: on press, on edit (op : TextOp).
claimClause : Lean.ParserDescr
claimBinder : Lean.ParserDescr
claimIn : Lean.ParserDescr
moveCmd : Lean.ParserDescr
flowCmd : Lean.ParserDescr
invariantCmd : Lean.ParserDescr
assumeCmd : Lean.ParserDescr
placeCmd : Lean.ParserDescr
retireCmd : Lean.ParserDescrA retired id: the claim is gone, its id stays issued.
movesTerm : Lean.ParserDescrThe moves declared in a namespace (the current one by default), as a list.
claimsTerm : Lean.ParserDescrThe ClaimInfo of every claim declared in a namespace (the current one by default),
including retired ids, ordered by id.
ref : Item → Lean.Syntax
key : Item → String
parseItem (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Item
parseClause (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM Item
refId (stx : Lean.Syntax) : ClaimId
read (body : Lean.Syntax) (allowed : List String) (kind : String) : Lean.Elab.Command.CommandElabM Clauses
prose? (c : Clauses) (n : String) : Option String
defn? (c : Clauses) (n : String) : Option (Lean.Syntax × Array Lean.Syntax × Lean.Term)
needDefn (items : Array Item) (ref : Lean.Syntax) (n what : String) (arity : Nat) : Lean.Elab.Command.CommandElabM (Array Lean.Syntax × Lean.Term)
A definition clause that must be present, with exactly arity binders.
optDefn (items : Array Item) (n : String) (arity : Nat) : Lean.Elab.Command.CommandElabM (Option (Array Lean.Syntax × Lean.Term))
needProse (c : Clauses) (ref : Lean.Syntax) (n what : String) : Lean.Elab.Command.CommandElabM String
checkTitle (ref : Lean.Syntax) (title : String) : Lean.Elab.Command.CommandElabM Unit
currentScope : Lean.CoreM StringThe package scope this module's claims are declared in (cairn.claims.scope).
checkFresh (ref : Lean.Syntax) (id : ClaimId) : Lean.Elab.Command.CommandElabM Unit
An id is issued once per scope in the whole imported environment.
checkPlace (stx : Lean.Syntax) : Lean.Elab.Command.CommandElabM (Option ClaimId)
checkUnsealed (ref : Lean.Syntax) (dispatched : Bool) : Lean.Elab.Command.CommandElabM Unit
register (e : Entry) : Lean.Elab.Command.CommandElabM Unit
lit (n : Nat) : Lean.Term
strLit (s : String) : Lean.Term
cid (n : Lean.Name) : Lean.Ident
binder (x : Lean.Syntax) (t : Lean.Term) : Lean.Elab.Command.CommandElabM (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
An explicit binder from a name the user wrote: an identifier, or a binderIdent (which may
be _).
mkDef (name : Lean.Name) (bs : Array (Lean.Syntax × Lean.Term)) (type body : Lean.Term) (doc : String := "") (reducible : Bool := false) : Lean.Elab.Command.CommandElabM Unit
def name binders : type := body, then its doc string.
mkThm (name : Lean.Name) (type proof : Lean.Term) (doc : String := "") : Lean.Elab.Command.CommandElabM Unit
foralls (bs : Array (Lean.Ident × Lean.Term)) (body : Lean.Term) : Lean.Elab.Command.CommandElabM Lean.Term
app (f : Lean.Name) (args : Array Lean.Term) : Lean.Term
mkInfo (name : Lean.Name) (id : ClaimId) (kind : Lean.Name) (title does sees : String) (place : Option ClaimId) (retired : Option String := none) : Lean.Elab.Command.CommandElabM Unit
docOf (doc? : Option Lean.Syntax) (fallback : String) : Lean.Elab.Command.CommandElabM String
triggers : List (String × Lean.Name)
elabMove : Lean.Elab.Command.CommandElab
stepAction (step : Lean.Syntax) : Lean.Elab.Command.CommandElabM (Lean.Term × ClaimId)
elabFlow : Lean.Elab.Command.CommandElab
decidableUnfolds (holds : Lean.Name) (SM : Lean.Term) : Lean.Elab.Command.CommandElabM (Option (Array Lean.Name))
The definitions to unfold, from holds down its body's head, before Decidable of the
property can be synthesized; none when it can't be, even after unfolding a few.
elabInvariant : Lean.Elab.Command.CommandElab
elabAssume : Lean.Elab.Command.CommandElab
elabPlace : Lean.Elab.Command.CommandElab
elabRetire : Lean.Elab.Command.CommandElab
nsOf (stx : Lean.Syntax) : Lean.Elab.TermElabM Lean.Name
elabMoves : Lean.Elab.Term.TermElab
elabClaims : Lean.Elab.Term.TermElab
Instances 1
instInhabitedItem : Inhabited Item
Syntax
The command keywords are not reserved: move, place and the rest stay usable as identifiers
(ClaimKind.place, a field called move). A plain &"move" is not found by the command
parser when it starts a command, so each keyword is a non-reserved symbol that also indexes
under identifiers.