max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: allow ?_

Browse source 
Note that `?_` is not equivalent to `_`. Both do not have a name, but
`?_` is a synthetic metavariable which **cannot** be assigned by typing
constraints, and `_` is a regular metavariable.
We use `?_` to mark an anonymous hole that must be filled using tactics.

@Kha I will rename `namedHole` to `syntheticHole`
This commit is contained in:
Leonardo de Moura 2020-08-30 07:54:34 -07:00
parent 825d9643cd
commit 89e0fa1488
3 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Term.lean
View file

@ -959,7 +959,8 @@ fun stx expectedType? => do
@[builtinTermElab «namedHole»] def elabNamedHole : TermElab :=
fun stx expectedType? => do
let name := stx.getIdAt 1;
let arg := stx.getArg 1;
let name := if arg.isIdent then arg.getId else Name.anonymous;
mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque name;
registerMVarErrorContext mvar.mvarId! stx;
pure mvar

10
src/Lean/Parser/Tactic.lean
View file

@ -65,11 +65,11 @@ def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 ma
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
/- Term binders as tactics. They are all implemented as macros using the triad: named holes, hygiene, and `refine` tactic. -/
@[builtinTacticParser] def «have» := parser! "have " >> Term.optIdent >> termParser >> (Term.haveAssign <|> Term.fromTerm) >> "; " >> tacticParser
@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.optIdent >> termParser >> Term.fromTerm >> "; " >> tacticParser
@[builtinTacticParser] def «show» := parser! "show " >> termParser >> " from " >> tacticParser
@[builtinTacticParser] def «let» := parser! "let " >> Term.letDecl >> "; " >> tacticParser
@[builtinTacticParser] def «let!» := parser! "let! " >> Term.letDecl >> "; " >> tacticParser
@[builtinTacticParser] def «have» := parser! "have " >> Term.haveDecl
@[builtinTacticParser] def «suffices» := parser! "suffices " >> Term.sufficesDecl
@[builtinTacticParser] def «show» := parser! "show " >> termParser
@[builtinTacticParser] def «let» := parser! "let " >> Term.letDecl
@[builtinTacticParser] def «let!» := parser! "let! " >> Term.letDecl
end Tactic
end Parser

8
src/Lean/Parser/Term.lean
View file

@ -53,7 +53,7 @@ def leadPrec := maxPrec - 1
@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
@[builtinTermParser] def prop := parser! "Prop"
@[builtinTermParser] def hole := parser! "_"
@[builtinTermParser] def namedHole := parser! "?" >> ident
@[builtinTermParser] def namedHole := parser! "?" >> (ident <|> hole)
@[builtinTermParser] def «sorry» := parser! "sorry"
@[builtinTermParser] def cdot := parser! "·"
@[builtinTermParser] def emptyC := parser! "∅"
@ -66,8 +66,10 @@ def optIdent : Parser := optional (try (ident >> " : "))
@[builtinTermParser] def «if» := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
def haveDecl := optIdent >> termParser >> (haveAssign <|> fromTerm)
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> haveDecl >> "; " >> termParser
def sufficesDecl := optIdent >> termParser >> fromTerm
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> sufficesDecl >> "; " >> termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> fromTerm
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)