Leonardo de Moura
d7c05a5ac4
fix: fixes #2042
2023-11-09 04:06:30 -08:00
int-y1
8d7520b36f
chore: fix typos in comments
2023-10-08 10:46:05 +02:00
Sebastian Ullrich
dc60150b5a
chore: update domain
2023-09-20 15:13:27 -07:00
Siddharth
b9ec36d089
chore: get rid of all inline C annotations for LLVM ( #2363 )
2023-07-30 10:39:40 +02:00
Gabriel Ebner
4af329588e
doc: clarify semi-out params
2023-04-10 13:00:04 -07:00
Gabriel Ebner
54c02d75b2
chore: let consumeTypeAnnotations remove semiOutParam
2023-04-10 13:00:04 -07:00
Evgenia Karunus
a125a36bcc
doc: Expr docs fix ( #2047 )
...
```
open Lean Meta
-- Docs text:
-- The let-expression `let x : Nat := 2; Nat.succ x` is represented as
def old : Expr :=
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.bvar 0) true
elab "old" : term => return old
#check old -- let x := 2; x : Nat
#reduce old -- 2
def new : Expr :=
Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
elab "new" : term => return new
#check new -- let x := 2; Nat.succ x : Nat
#reduce new -- 3
```
2023-01-20 09:51:55 +01:00
Leonardo de Moura
0a031fc9bb
chore: replace Expr.forEach with Expr.forEachWhere
2022-12-01 05:19:32 -08:00
Leonardo de Moura
8f40899cde
feat: add Expr.updateFVar!
2022-11-07 16:18:35 -08:00
Gabriel Ebner
dcc97c9bbe
fix: preserve sharing in instantiateLevelParams
2022-10-24 12:23:13 -07:00
Mario Carneiro
583e023314
chore: snake-case attributes (part 2)
2022-10-19 09:28:08 -07:00
Leonardo de Moura
641fa77738
chore: minimize the number of red-black insert specializations
2022-10-16 16:20:46 -07:00
Gabriel Ebner
ba57ad3480
feat: add implementation-detail hypotheses
2022-10-11 17:24:35 -07:00
Mario Carneiro
b6a58d13e1
fix: LHS goals should be pre-whnf'd
2022-09-28 14:24:44 -07:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Yuri de Wit
c65a206d6a
chore: reintroduced 'important' let paragraph
2022-09-21 07:36:25 -07:00
Yuri de Wit
64a0ec91fa
chore: few updates to Expr documentation
2022-09-21 07:36:25 -07:00
Leonardo de Moura
631c216bab
fix: LCNF pretty printer missing parens
2022-09-20 15:51:32 -07:00
Yuri de Wit
88fc24c58c
chore: fixed typos
2022-09-19 08:14:37 -07:00
Gabriel Ebner
f1b5fa53f0
chore: use new comment syntax
2022-09-14 08:26:17 -07:00
Leonardo de Moura
e78820e6a5
feat: add mkFixedArgMap
2022-09-11 20:19:44 -07:00
Sebastian Ullrich
e81ba951c6
fix: Core.transform API and uses
2022-08-25 19:07:42 -07:00
Leonardo de Moura
ec7b5c6c2a
chore: remove redundant data form Expr.Data
2022-07-29 21:25:03 -07:00
Leonardo de Moura
d0d5effcbc
doc: update doc string
2022-07-28 09:48:46 -07:00
Leonardo de Moura
0d43684956
chore: fix some docstrings
2022-07-27 06:46:00 -07:00
Leonardo de Moura
a62949c49b
refactor: add type LevelMVarId (and abbreviation LMarId)
...
Motivation: make sure we do not mixup metavariable ids for
expression and universe level.
cc @bollu
2022-07-24 17:21:45 -07:00
Gabriel Ebner
eda3eae18e
perf: implement Expr.update* in Lean
2022-07-19 05:55:13 -07:00
Leonardo de Moura
d95163641a
chore: indent docstrings
2022-07-18 22:36:55 -04:00
Leonardo de Moura
7331fdf310
doc: Expr.lean
2022-07-17 17:28:28 -04:00
Leonardo de Moura
7cb011e94c
doc: Expr.lean
2022-07-17 14:49:55 -04:00
Gabriel Ebner
a8cab84735
refactor: use computed fields for Expr
2022-07-11 14:19:41 -07:00
Leonardo de Moura
ba606debf7
fix: Expr.update* issue
...
See #1291
2022-07-10 08:33:14 -07:00
E.W.Ayers
562070fe8b
refactor: more extract methods from transform
2022-06-17 17:47:51 -07:00
Leonardo de Moura
02c4e548df
feat: replace constant with opaque
2022-06-14 17:02:59 -07:00
Sebastian Ullrich
fb2a2b3de2
fix: fixup previous commit
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Leonardo de Moura
e552558f2f
chore: style
2022-05-23 11:04:29 -07:00
Leonardo de Moura
ab31f9ad5d
fix: fixes #1143
2022-05-07 15:27:34 -07:00
Leonardo de Moura
3cf425ba52
fix: pattern hover information
...
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
2022-04-08 15:03:42 -07:00
Leonardo de Moura
4793c7e734
feat: add isAppOfArity variant that skips Expr.mdata
2022-04-08 15:01:57 -07:00
Leonardo de Moura
152eff5cea
chore: missing double ticks
2022-04-08 15:01:57 -07:00
E.W.Ayers
24ebd78071
doc: Expr.lean
2022-03-24 14:52:09 -07:00
Leonardo de Moura
e44b36cab0
chore: cleanup optimization using Lean bitwise operators
2022-03-15 12:06:08 -07:00
Leonardo de Moura
d3e2dfb079
perf: optimize mkApp
2022-03-15 11:31:15 -07:00
Leonardo de Moura
9d73317d76
perf: faster Expr.data
2022-03-15 11:30:41 -07:00
Leonardo de Moura
5283007aa4
feat: add HasConstCache
2022-03-15 08:39:48 -07:00
Leonardo de Moura
4e261b15e5
fix: smart unfolding bug in over applications
2022-03-14 19:17:21 -07:00
Leonardo de Moura
33883e9d2a
fix: resulting type of projection functions should not include auxiliary type annotations (e.g., autoParam)
2022-03-10 07:47:38 -08:00
Leonardo de Moura
5825eb394f
refactor: move isOutParam to Expr.lean, rename consumeAutoOptParam => consumeTypeAnnotations
2022-03-10 07:37:41 -08:00
