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

feat: doc comment support for unif_hint

Browse source
This commit is contained in:
Sebastian Ullrich 2022-07-22 13:36:53 +02:00
parent ce0a0166e8
commit 1f081ee6cb
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Init/NotationExtra.lean
View file

@ -64,15 +64,15 @@ def expandBrackedBinders (combinatorDeclName : Name) (bracketedExplicitBinders :
syntax unifConstraint := term (" =?= " <|> " ≟ ") term
syntax unifConstraintElem := colGe unifConstraint ", "?
syntax attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
syntax (docComment)? attrKind "unif_hint " (ident)? bracketedBinder* " where " withPosition(unifConstraintElem*) ("|-" <|> "⊢ ") unifConstraint : command
macro_rules
| `($kind:attrKind unif_hint $(n)? $bs:bracketedBinder* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
| `($[$doc?:docComment]? $kind:attrKind unif_hint $(n)? $bs* where $[$cs₁:term ≟ $cs₂]* |- $t₁:term ≟ $t₂) => do
let mut body ← `($t₁ = $t₂)
for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do
body ← `($c₁ = $c₂ → $body)
let hint : Ident ← `(hint)
`(@[$kind:attrKind unificationHint] def $(n.getD hint):ident $bs:bracketedBinder* : Sort _ := $body)
`($[$doc?:docComment]? @[$kind:attrKind unificationHint] def $(n.getD hint) $bs:bracketedBinder* : Sort _ := $body)
end Lean
open Lean

1
tests/lean/run/unifhint1.lean
View file

@ -16,6 +16,7 @@ instance : CoeSort Magma.{u} (Type u) where
def mul {s : Magma} (a b : s) : s :=
s.mul a b
/-- hi -/
unif_hint (s : Magma) where
s =?= Nat.Magma |- s.α =?= Nat