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

feat: add HasQuote for Option

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-14 18:03:33 -08:00
parent 35213b63ae
commit e7db119948
1 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Init/Lean/Elab/Quotation.lean
View file

@ -39,23 +39,29 @@ private def quoteName : Name → Syntax
| Name.str n s _ => Unhygienic.run `(_root_.Lean.mkNameStr $(quoteName n) $(quote s))
| Name.num n i _ => Unhygienic.run `(_root_.Lean.mkNameNum $(quoteName n) $(quote i))
instance Name.HasQuote : HasQuote Name := ⟨quoteName⟩
instance Name.hasQuote : HasQuote Name := ⟨quoteName⟩
private def appN (fn : Syntax) (args : Array Syntax) : Syntax :=
args.foldl (fun fn arg => Unhygienic.run `($fn $arg)) fn
instance Prod.HasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
instance Prod.hasQuote {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) :=
⟨fun ⟨a, b⟩ => Unhygienic.run `(_root_.Prod.mk $(quote a) $(quote b))⟩
private def quoteList {α : Type} [HasQuote α] : List α → Syntax
| [] => Unhygienic.run `(_root_.List.nil)
| (x::xs) => Unhygienic.run `(_root_.List.cons $(quote x) $(quoteList xs))
instance List.HasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
instance List.hasQuote {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩
instance Array.HasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
instance Array.hasQuote {α : Type} [HasQuote α] : HasQuote (Array α) :=
⟨fun xs => let stx := quote xs.toList; Unhygienic.run `(_root_.List.toArray $stx)⟩
private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax
| none => Unhygienic.run `(_root_.Option.none)
| (some x) => Unhygienic.run `(_root_.Option.some $(quote x))
instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩
namespace Elab
namespace Term