Documentation

Allow implicit type declarations

Disallow implicit type declarations

Implicits hare are scoped rather than top level

Allow scoped constraint arguments

Parses an expression as a whole FullExpr ::= Expr EOF_t;

Parses an expression Expr ::= Pi

Parses an expression with possible operator applied OpExpr ::= ;

Parses either an internally defined expression or a user-defined one Expr' ::= "External (User-defined) Syntax" | InternalExpr;

Parses a user-defined expression

Parses a simple user-defined expression

Tries to parse a user-defined expression given a list of syntactic extensions

Parses a (normal) built-in expression InternalExpr ::= UnifyLog | RecordType | SimpleExpr | Lambda | QuoteGoal | Let | If | RewriteTerm | CaseExpr | DoBlock | App ;

Parses the "impossible" keyword Impossible ::= impossible

Parses a case expression CaseExpr ::= 'case' Expr 'of' OpenBlock CaseOption+ CloseBlock;

Parses a case in a case expression CaseOption ::= Expr (Impossible | '=>' Expr) Terminator ;

Parses a proof block ProofExpr ::= proof OpenBlock Tactic'* CloseBlock ;

Parses a tactics block TacticsExpr := tactics OpenBlock Tactic'* CloseBlock ;

Parses a simple expression @ SimpleExpr ::=

| ? Name | % implementation | Refl ('{' Expr '}')? | ProofExpr | TacticsExpr | FnName | Idiom | List | Alt | Bracketed | Constant | Type | Void | Quasiquote | NameQuote | Unquote | '_' ; @

Parses an expression in parentheses Bracketed ::= '(' Bracketed'

Parses the rest of an expression in braces Bracketed' ::= ')' | Expr ')' | ExprList ')' | DependentPair ')' | Operator Expr ')' | Expr Operator ')' ;

Parses the rest of a dependent pair after '(' or '(Expr **'

Parse the contents of parentheses, after an expression has been parsed.

Finds optimal type for integer constant

Parses an alternative expression @ Alt ::= '(|' Expr_List '|)';

Expr_List ::= Expr' | Expr' ',' Expr_List ; @

Parses a possibly hidden simple expression HSimpleExpr ::= . SimpleExpr | SimpleExpr ;

Parses a unification log expression UnifyLog ::= % unifyLog SimpleExpr ;

Parses a new-style tactics expression RunTactics ::= % runElab SimpleExpr ;

Parses a disambiguation expression Disamb ::= with NameList Expr ;

Parses a no implicits expression NoImplicits ::= % noImplicits SimpleExpr ;

Parses a function application expression App ::= mkForeign Arg Arg* | MatchApp | SimpleExpr Arg* ; MatchApp ::= SimpleExpr <== FnName ;

Parses a function argument Arg ::= ImplicitArg | ConstraintArg | SimpleExpr ;

Parses an implicit function argument ImplicitArg ::= '{' Name ('=' Expr)? '}' ;

Parses a constraint argument (for selecting a named interface implementation)

   ConstraintArg ::=
     '@{' Expr '}'
     ;

Parses a quasiquote expression (for building reflected terms using the elaborator)

Quasiquote ::= '`(' Expr ')'

Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

Unquote ::= ',' Expr

Parses a quotation of a name (for using the elaborator to resolve boring details)

NameQuote ::= '`{' Name '}'

Parses a record field setter expression RecordType ::= record '{' FieldTypeList '}'; FieldTypeList ::= FieldType | FieldType ',' FieldTypeList ; FieldType ::= FnName '=' Expr ;

Creates setters for record types on necessary functions

Parses a type signature TypeSig ::= : Expr ; TypeExpr ::= ConstraintList? Expr;

Parses a lambda expression Lambda ::= \\ TypeOptDeclList LambdaTail | \\ SimpleExprList LambdaTail ; SimpleExprList ::= SimpleExpr | SimpleExpr ',' SimpleExprList ; LambdaTail ::= Impossible | '=>' Expr

Parses a term rewrite expression RewriteTerm ::= rewrite Expr (==> Expr)? 'in' Expr ;

Parses a let binding @ Let ::= 'let' Name TypeSig'? '=' Expr 'in' Expr | 'let' Expr' '=' Expr' 'in' Expr

TypeSig' ::= : Expr' ; @

Parses a conditional expression If ::= 'if' Expr 'then' Expr 'else' Expr

Parses a quote goal

QuoteGoal ::=
  quoteGoal Name by Expr 'in' Expr
  ;

Parses a dependent type signature

Pi ::= PiOpts Static? Pi'

Pi' ::=
    OpExpr ('->' Pi)?
  | '(' TypeDeclList           ')'            '->' Pi
  | '{' TypeDeclList           '}'            '->' Pi
  | '{' auto    TypeDeclList '}'            '->' Pi
  | '{' 'default' SimpleExpr TypeDeclList '}' '->' Pi
  ;

Parses Possible Options for Pi Expressions PiOpts ::= .?

Parses a type constraint list

ConstraintList ::=
    '(' Expr_List ')' '=>'
  | Expr              '=>'
  ;

Parses a type declaration list TypeDeclList ::= FunctionSignatureList | NameList TypeSig ;

FunctionSignatureList ::=
    Name TypeSig
  | Name TypeSig ',' FunctionSignatureList
  ;

Parses a type declaration list with optional parameters TypeOptDeclList ::= NameOrPlaceholder TypeSig? | NameOrPlaceholder TypeSig? ',' TypeOptDeclList ;

NameOrPlaceHolder ::= Name | '_';

Parses a list literal expression e.g. [1,2,3] or a comprehension [ (x, y) | x <- xs , y <- ys ] ListExpr ::= '[' ']' | '[' Expr '|' DoList ']' | '[' ExprList ']' ; DoList ::= Do | Do ',' DoList ; ExprList ::= Expr | Expr ',' ExprList ;

Parses a do-block Do' ::= Do KeepTerminator;

DoBlock ::=
  'do' OpenBlock Do'+ CloseBlock
  ;

Parses an expression inside a do block Do ::= 'let' Name TypeSig'? '=' Expr | 'let' Expr' '=' Expr | 'rewrite Expr | Name '<-' Expr | Expr' '<-' Expr | Expr ;

Parses an expression in idiom brackets Idiom ::= '[|' Expr '|]';

Parses a constant or literal expression

Constant ::=
    Integer
  | Int
  | Char
  | Double
  | String
  | Bits8
  | Bits16
  | Bits32
  | Bits64
  | Float_t
  | Natural_t
  | VerbatimString_t
  | String_t
  | Char_t
  ;

Parse a constant and its source span

Parses a verbatim multi-line string literal (triple-quoted)

VerbatimString_t ::=
  '"""' ~'"""' '"'* '"""'
;

Parses a static modifier

Static ::=
  '%static'
;

Parses a tactic script

Tactic ::= intro NameList?
       |   intros
       |   refine      Name Imp+
       |   mrefine     Name
       |   rewrite     Expr
       |   induction   Expr
       |   equiv       Expr
       |   'let'         Name : Expr' '=' Expr
       |   'let'         Name           '=' Expr
       |   focus       Name
       |   exact       Expr
       |   applyTactic Expr
       |   reflect     Expr
       |   fill        Expr
       |   try         Tactic '|' Tactic
       |   '{' TacticSeq '}'
       |   compute
       |   trivial
       |   solve
       |   attack
       |   state
       |   term
       |   undo
       |   qed
       |   abandon
       |   : q
       ;

Imp ::= ? | '_';

TacticSeq ::=
    Tactic ';' Tactic
  | Tactic ';' TacticSeq
  ;

A specification of the arguments that tactics can take

A list of available tactics and their argument requirements

Parses a tactic as a whole