3770b3dcb8
This PR fixed typos: ``` pip install codespell --upgrade codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex '[A-Z][a-z]*' codespell --summary --ignore-words-list enew,forin,fro,happend,hge,ihs,iterm,spred --skip stage0 --check-filenames --regex "\b[a-z']*" ```
60 lines
1.2 KiB
Text
60 lines
1.2 KiB
Text
#eval (1,(2,3)).2.fst
|
||
|
||
#check 31.
|
||
#check 31.0
|
||
#eval 31.
|
||
#eval 31.0
|
||
|
||
#check 31.e
|
||
#check 31.ee
|
||
|
||
#check 31.f
|
||
#check 31.ff
|
||
|
||
#check 31.3e
|
||
#check 31.3e2
|
||
#check 31.3ee2
|
||
|
||
#check 31.3f
|
||
#check 31.3f2
|
||
#check 31.3ff2
|
||
|
||
#check 11.toDigits 13
|
||
#check (11).toDigits 13
|
||
#eval (11).toDigits 13
|
||
#check (11).toDigits(13)
|
||
#check (11).toDigits (13)
|
||
|
||
def succ (a: Nat) := a + 1
|
||
def foo {A B} (_: A) (_: B) : Unit := ()
|
||
#check foo 31.succ
|
||
#check foo (31).succ
|
||
#check foo 31(.succ)
|
||
#check foo (31)(.succ)
|
||
#check foo 31 .succ
|
||
#check foo 31. succ
|
||
|
||
#check 11succ
|
||
#check 11.succ
|
||
#check 11.12succ
|
||
#check (11.succ)
|
||
#check (11.12succ)
|
||
|
||
|
||
-- This example (adapted from structInst4.lean) exercises the difference between
|
||
-- term parsing and LVal parsing; the latter fails if we allow `2.snd` to parse
|
||
-- as a scientificLit followed by an error token, so this test captures
|
||
-- that we have to throw the error token right away, positioned before, rather
|
||
-- than after the `2.`
|
||
structure Foo where
|
||
(x : Nat × (Nat × Nat) := (2, (4, 5)))
|
||
def bar : Foo := {}
|
||
#check bar.x.2.snd
|
||
#eval { bar with x.2.snd := 1 }
|
||
|
||
inductive Nope where
|
||
| succ : Nope -> Nope -> Nope
|
||
| leaf : Nope
|
||
|
||
example := (match · with
|
||
| succ x y => 4)
|