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

chore: add test for sepByIndent.formatter

Browse source
This commit is contained in:
Gabriel Ebner 2022-06-23 21:50:18 +02:00 • committed by Sebastian Ullrich
parent d5142ddeb8
commit 233a787e65
2 changed files with 22 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/lean/sepByIndentQuot.lean Normal file
View file

@ -0,0 +1,16 @@
import Lean
open Lean Elab
#eval show TermElabM _ from do
let x ← `(x)
let xs := #[x,x,x,x]
let ys := xs
PrettyPrinter.ppTerm <|<-
`(frobnicate { $[$xs:ident := $ys:term],* })
#eval show TermElabM _ from do
let x ← `(x)
let xs := #[x,x,x,x]
let ys := xs
PrettyPrinter.ppTerm <|<-
`(frobnicate { $[$xs:ident := $ys:term]* })

6
tests/lean/sepByIndentQuot.lean.expected.out Normal file
View file

@ -0,0 +1,6 @@
frobnicate✝ { x✝ := x✝, x✝ := x✝, x✝ := x✝, x✝ := x✝ }
frobnicate✝ {
x✝ := x✝
x✝ := x✝
x✝ := x✝
x✝ := x✝ }