issues
search
leanprover-community
/
quote4
Intuitive, type-safe expression quotations for Lean 4.
Apache License 2.0
73
stars
11
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
chore: merge bump/v4.12.0 and move toolchain to v4.12.0-rc1
#56
semorrison
closed
4 days ago
0
chore: bump toolchain to v4.11.0
#55
semorrison
closed
5 days ago
0
chore: remove unnecessary 'open'; compatibility with v4.11.0-rc3
#54
semorrison
closed
1 week ago
0
chore: use new HashMap
#53
semorrison
closed
4 days ago
0
linter.constructorNameAsVariable false in turnExistsIntoForall
#52
awalterschulze
opened
2 weeks ago
1
chore: replace a product with a structure
#51
eric-wieser
opened
2 weeks ago
0
Fix #16
#50
eric-wieser
opened
2 weeks ago
0
Bump to Lean v4.10.0
#49
eric-wieser
closed
4 weeks ago
0
chore: adaptations for nightly-2024-08-08
#48
semorrison
closed
4 weeks ago
0
doc: Add module docstrings and info about `~q()`
#47
eric-wieser
closed
1 month ago
4
chore: switch from lakefile.lean to lakefile.toml
#46
semorrison
opened
2 months ago
0
Reductive behaviour changed recently
#45
javra
closed
2 months ago
1
chore: move to v4.9.0-rc1
#44
semorrison
closed
3 months ago
0
chore: adaptations for nightly-2024-05-09
#43
semorrison
closed
3 months ago
0
feat: add lake-manifest.json, update .gitignore
#42
Shreyas4991
closed
4 months ago
1
fix: workaround leanprover/lean4#3827
#41
eric-wieser
closed
5 months ago
1
chore: update .gitignore for modern lake
#40
semorrison
closed
5 months ago
0
chore: don't use String->Name coercion, which may be removed
#39
semorrison
closed
5 months ago
0
assertInstancesCommute loops when there are several unnamed assumptions
#38
dwrensha
opened
6 months ago
1
Poor elaboration performance on structure matches
#37
eric-wieser
opened
6 months ago
0
`let mut` does not work with `~q` matching
#36
eric-wieser
opened
6 months ago
0
doc: promote field comments to docstrings
#35
eric-wieser
closed
6 months ago
1
literal expressions not type-safe
#34
ericrbg
opened
7 months ago
0
add support for the no-op `generalizing := true`
#33
eric-wieser
closed
6 months ago
1
Bump to Lean v4.6.0-rc1 and add tests for #31
#32
eric-wieser
closed
7 months ago
0
fix: do not introduce additional `let`s that block match generalization
#31
eric-wieser
closed
8 months ago
1
invalid match-expression, type of pattern variable 'match_eq✝' contains metavariables
#30
eric-wieser
opened
8 months ago
3
`generalizing` does not work in `match`
#29
eric-wieser
closed
6 months ago
1
Fix: use exprToSyntax in `comefrom` elaborator
#28
kmill
closed
9 months ago
1
Attempt to fix #21
#27
eric-wieser
opened
9 months ago
0
fix: correct matching on sigma types
#26
eric-wieser
closed
9 months ago
2
chore: add lakefile.olean to .gitignore
#25
semorrison
closed
10 months ago
1
chore: bump toolchain to v4.0.0
#24
semorrison
closed
11 months ago
0
License under Apache2 to match mathlib
#23
eric-wieser
closed
11 months ago
2
chore: bump to nightly-2023-08-19
#22
semorrison
closed
1 year ago
1
`~q` pattern match does not respect `return`
#21
Vtec234
opened
1 year ago
4
chore: don't rely on autogenerated instance names
#20
semorrison
closed
1 year ago
1
Potential unhygienic use of functions in `Lean` namespace
#19
Vtec234
closed
1 year ago
2
Incorrect delaboration of antiquotations with functions that don't reduce
#18
Vtec234
closed
1 year ago
4
Universe issue in dependent `PSigma`
#17
Vtec234
closed
1 year ago
0
`foo.{$u}` is not supported
#16
Vtec234
opened
1 year ago
0
Confusing type of `Expr` inputs in the local context
#15
Vtec234
opened
1 year ago
0
fix: typo in binder
#14
Vtec234
closed
10 months ago
2
`maximum recursion depth` error
#13
javra
closed
1 year ago
3
Deep matching like Ltac's context
#12
awalterschulze
opened
1 year ago
0
Ensure shadowed variables are inaccessible in quotations
#11
alexkeizer
opened
1 year ago
2
Add type variables to unquote context, if they implement `ToExpr`
#10
alexkeizer
closed
1 year ago
0
Antiquotations don't work for generic types (even if they implement ToExpr)
#9
alexkeizer
opened
1 year ago
0
Weird `unknown free variable '_uniq.419'` error
#8
alexkeizer
opened
1 year ago
0
error: unknown identifier 'resettingSynthInstanceCache' on Lean nightly with fresh package.
#7
debordle
closed
1 year ago
1
Next