8000 Commits · cppio/lean4 · GitHub

More Web Proxy on the site http://driver.im/

Commits

Commits on Sep 23, 2024

fix: must not reduce `ite` in the discriminant of match-expression when reducibility setting is `.reducible` (#5419)
leodemoura
authored

Commits on Sep 20, 2024

fix: modify projection instance binder info (#5376)

authored

Commits on Sep 2, 2024

chore: use `Expr.numObjs` instead of `lean_expr_size_shared` (#5239)
leodemoura
authored

Commits on Sep 1, 2024

perf: maximize term sharing at `instantiateMVarDeclMVars` (#5226)
leodemoura
authored
perf: cache visited exprs at `CheckAssignmentQuick` (#5225)
leodemoura
authored

Commits on Aug 12, 2024

Commits on Aug 7, 2024

Commits on Aug 6, 2024

Commits on Aug 4, 2024

Commits on Aug 3, 2024

perf: use `NatPow Int` instead of `HPow Int Nat Int` (#4903)
leodemoura
authored

Commits on Aug 1, 2024

perf: precise cache for `expr_eq_fn` (#4890)
leodemoura
authored

Commits on Jul 31, 2024

refactor: `sharecommon` (#4887)
leodemoura
authored

Commits on Jul 30, 2024

perf: precise cache for `foldConsts` (#4871)
leodemoura
authored

Commits on Jul 19, 2024

fix: add term elaborator for `Lean.Parser.Term.namedPattern` (#4792)
leodemoura
authored

0