Code

merge#486

Code

Merged

xiyuzhai merged 206 commits intoxiyuzhai-husky-lang:mainxiyuzhai-husky-lang/husky:mainfrom xiyuzhai:mainxiyuzhai/husky:mainCopy head branch name to clipboardJan 9, 2025

+12,553-2,813

Commits

Commits on Dec 30, 2024

• init mathlib4 tests in standard linear elaborator

  xiyuzhai

  committed
  bc7ee6b

  Copy full SHA for bc7ee6b

• save

  xiyuzhai

  committed
  2cfdd7a

  Copy full SHA for 2cfdd7a

• save

  xiyuzhai

  committed
  afb2002

  Copy full SHA for afb2002

Commits on Dec 31, 2024

• save

  xiyuzhai

  committed
  bf6f2a6

  Copy full SHA for bf6f2a6

• save

  xiyuzhai

  committed
  6c282e7

  Copy full SHA for 6c282e7

• init generalized-aho-corasick

  xiyuzhai

  committed
  c4258b7

  Copy full SHA for c4258b7

• save

  xiyuzhai

  committed
  ae35161

  Copy full SHA for ae35161

• save

  xiyuzhai

  committed
  8f042fb

  Copy full SHA for 8f042fb

• improve docs

  xiyuzhai

  committed
  9fed44f

  Copy full SHA for 9fed44f

• feat: string_prefix_trie_with_gac_dfs_sequential_engine_works

  xiyuzhai

  committed
  75a7b8b

  Copy full SHA for 75a7b8b

• fix tests

  xiyuzhai

  committed
  2a7860f

  Copy full SHA for 2a7860f

• update expects

  xiyuzhai

  committed
  68a783c

  Copy full SHA for 68a783c

• rename linear to sequential

  xiyuzhai

  committed
  9149f7a

  Copy full SHA for 9149f7a

• rename

  xiyuzhai

  committed
  4b2a3ff

  Copy full SHA for 4b2a3ff

• rename visored-tactic-standard-sequential-elaborator to visored-mir-standard-sequential-elaborator

  xiyuzhai

  committed
  b12bf5a

  Copy full SHA for b12bf5a

• rename

  xiyuzhai

  committed
  9b671b0

  Copy full SHA for 9b671b0

• overhaul

  xiyuzhai

  committed
  060f905

  Copy full SHA for 060f905

• save

  xiyuzhai

  committed
  3f4bbc3

  Copy full SHA for 3f4bbc3

• save

  xiyuzhai

  committed
  e4dfd6a

  Copy full SHA for e4dfd6a

• save

  xiyuzhai

  committed
  b3ef689

  Copy full SHA for b3ef689

• reinstate tactics

  xiyuzhai

  committed
  15ec8e7

  Copy full SHA for 15ec8e7

• add qed stmt

  xiyuzhai

  committed
  7e4d3fe

  Copy full SHA for 7e4d3fe

• save

  xiyuzhai

  committed
  b810085

  Copy full SHA for b810085

• save

  xiyuzhai

  committed
  bfc58d4

  Copy full SHA for bfc58d4

• save

  xiyuzhai

  committed
  da1d995

  Copy full SHA for da1d995

• remove unnecessary obvious tactic

  xiyuzhai

  committed
  fab1574

  Copy full SHA for fab1574

• save

  xiyuzhai

  committed
  1c82059

  Copy full SHA for 1c82059

Commits on Jan 1, 2025

• rename floated to floated-parallel

  xiyuzhai

  committed
  d886305

  Copy full SHA for d886305

• feat: floated-sequential seems to work

  xiyuzhai

  committed
  1944ad7

  Copy full SHA for 1944ad7

• renamed visored-mir-basic-elaborator to visored-baseq-elaborator

  xiyuzhai

  committed
  caf8062

  Copy full SHA for caf8062

• save

  xiyuzhai

  committed
  8802e12

  Copy full SHA for 8802e12

• fix lifetime issues in floated

  xiyuzhai

  committed
  5b55a30

  Copy full SHA for 5b55a30

• fix lifetime issues in floated

  xiyuzhai

  committed
  42f4cbc

  Copy full SHA for 42f4cbc

• intro hypothesis to visored elaborator

  xiyuzhai

  committed
  a7c3ce5

  Copy full SHA for a7c3ce5

• save

  xiyuzhai

  committed
  f3390ce

  Copy full SHA for f3390ce

• save

  xiyuzhai

  committed
  3777563

  Copy full SHA for 3777563

• save

  xiyuzhai

  committed
  455dc65

  Copy full SHA for 455dc65

• rename builder to constructor for hypothesis

  xiyuzhai

  committed
  c0eddbb

  Copy full SHA for c0eddbb

Commits on Jan 2, 2025

• save

  xiyuzhai

  committed
  68d7334

  Copy full SHA for 68d7334

• save

  xiyuzhai

  committed
  bb2f9be

  Copy full SHA for bb2f9be

• save

  xiyuzhai

  committed
  e36342e

  Copy full SHA for e36342e

• save

  xiyuzhai

  committed
  fcd4f35

  Copy full SHA for fcd4f35

• save

  xiyuzhai

  committed
  dcbee3f

  Copy full SHA for dcbee3f

• save

  xiyuzhai

  committed
  b4beb64

  Copy full SHA for b4beb64

• save

  xiyuzhai

  committed
  83e6c1d

  Copy full SHA for 83e6c1d

• add typing to expr

  xiyuzhai

  committed
  93dd206

  Copy full SHA for 93dd206

• save

  xiyuzhai

  committed
  7cc37d2

  Copy full SHA for 7cc37d2

• save

  xiyuzhai

  committed
  26a3dc0

  Copy full SHA for 26a3dc0

• save

  xiyuzhai

  committed
  169e67e

  Copy full SHA for 169e67e

• save

  xiyuzhai

  committed
  1ee544b

  Copy full SHA for 1ee544b

• save

  xiyuzhai

  committed
  aa934b8

  Copy full SHA for aa934b8

• save

  xiyuzhai

  committed
  3ef0977

  Copy full SHA for 3ef0977

• feat: visored-baseq-elaborator works for the first time!

  xiyuzhai

  committed
  bccff82

  Copy full SHA for bccff82

Commits on Jan 3, 2025

• separate out assume from let placeholder

  xiyuzhai

  committed
  4854553

  Copy full SHA for 4854553

• fix: goal collection

  xiyuzhai

  committed
  f6a32af

  Copy full SHA for f6a32af

• try add apply

  xiyuzhai

  committed
  4939466

  Copy full SHA for 4939466

• save

  xiyuzhai

  committed
  443958c

  Copy full SHA for 443958c

• impl debug for expr fld

  xiyuzhai

  committed
  d5e974c

  Copy full SHA for d5e974c

• feat: visored tactic works for the very first time

  xiyuzhai

  committed
  fe19fbd

  Copy full SHA for fe19fbd

• put imports out of tracker

  xiyuzhai

  committed
  c2bf2b8

  Copy full SHA for c2bf2b8

Commits on Jan 4, 2025

• add coercion to visored elaborator

  xiyuzhai

  committed
  614b974

  Copy full SHA for 614b974

• rename to prune for clarity

  xiyuzhai

  committed
  2c5abac

  Copy full SHA for 2c5abac

• save

  xiyuzhai

  committed
  2a785ca

  Copy full SHA for 2a785ca

• save

  xiyuzhai

  committed
  59031d1

  Copy full SHA for 59031d1

• save

  xiyuzhai

  committed
  a933f54

  Copy full SHA for a933f54

• save

  xiyuzhai

  committed
  71c62f0

  Copy full SHA for 71c62f0

• save

  xiyuzhai

  committed
  638f6e1

  Copy full SHA for 638f6e1

• save

  xiyuzhai

  committed
  d9c805c

  Copy full SHA for d9c805c

• save

  xiyuzhai

  committed
  5b59102

  Copy full SHA for 5b59102

• save

  xiyuzhai

  committed
  9017995

  Copy full SHA for 9017995

• save

  xiyuzhai

  committed
  336752b

  Copy full SHA for 336752b

Commits on Jan 5, 2025

• terms

  xiyuzhai

  committed
  ca7bfe3

  Copy full SHA for ca7bfe3

• save

  xiyuzhai

  committed
  e0a8b5d

  Copy full SHA for e0a8b5d

• save

  xiyuzhai

  committed
  bd863f6

  Copy full SHA for bd863f6

• save

  xiyuzhai

  committed
  622a347

  Copy full SHA for 622a347

• save

  xiyuzhai

  committed
  cfd1fb5

  Copy full SHA for cfd1fb5

• save

  xiyuzhai

  committed
  80f5613

  Copy full SHA for 80f5613

• save

  xiyuzhai

  committed
  e6cb5e2

  Copy full SHA for e6cb5e2

• save

  xiyuzhai

  committed
  1eb0e79

  Copy full SHA for 1eb0e79

• save

  xiyuzhai

  committed
  dfa875d

  Copy full SHA for dfa875d

• init miracle

  xiyuzhai

  committed
  87238f8

  Copy full SHA for 87238f8

• towards fixing visored lean transpilation

  xiyuzhai

  committed
  da37199

  Copy full SHA for da37199

• mythic bug

  xiyuzhai

  committed
  56a7bb5

  Copy full SHA for 56a7bb5

• fix bug

  xiyuzhai

  committed
  35536c1

  Copy full SHA for 35536c1

• save

  xiyuzhai

  committed
  951a7b3

  Copy full SHA for 951a7b3

• feat: 0=0

  xiyuzhai

  committed
  8c34d1b

  Copy full SHA for 8c34d1b

• 0<1

  xiyuzhai

  committed
  40d9afb

  Copy full SHA for 40d9afb

• $0\ne 1$

  xiyuzhai

  committed
  9478d7d

  Copy full SHA for 9478d7d

• save

  xiyuzhai

  committed
  54403c1

  Copy full SHA for 54403c1

• feat: 1+1=2

  xiyuzhai

  committed
  f5de5b6

  Copy full SHA for f5de5b6

• strange bug

  xiyuzhai

  committed
  8c1dfe3

  Copy full SHA for 8c1dfe3

• fix jar key bug in eterned/floated; fix qed transpilation

  xiyuzhai

  committed
  df31b1d

  Copy full SHA for df31b1d

Commits on Jan 6, 2025

• save

  xiyuzhai

  committed
  10b7287

  Copy full SHA for 10b7287

• add split to Miracle

  xiyuzhai

  committed
  e60a4b7

  Copy full SHA for e60a4b7

• init alt-maybe-result

  xiyuzhai

  committed
  399bbdf

  Copy full SHA for 399bbdf

• fix doctest

  xiyuzhai

  committed
  f6a85fe

  Copy full SHA for f6a85fe

• apply alt-maybe-result to miracle

  xiyuzhai

  committed
  a90dc0a

  Copy full SHA for a90dc0a

• init miracle fold

  xiyuzhai

  committed
  44cbf1a

  Copy full SHA for 44cbf1a

• x - x = 0

  xiyuzhai

  committed
  7c13bea

  Copy full SHA for 7c13bea

• x + x = 2x

  xiyuzhai

  committed
  4018d51

  Copy full SHA for 4018d51

• new crate monadic-fold

  xiyuzhai

  committed
  ef6da22

  Copy full SHA for ef6da22

• save

  xiyuzhai

  committed
  4be5084

  Copy full SHA for 4be5084

• save

  xiyuzhai

  committed
  4308882

  Copy full SHA for 4308882

• feat: intro visored-mir-opr

  xiyuzhai

  committed
  0d514a5

  Copy full SHA for 0d514a5

• save

  xiyuzhai

  committed
  444ea2c

  Copy full SHA for 444ea2c

• save

  xiyuzhai

  committed
  8adf783

  Copy full SHA for 8adf783

• save

  xiyuzhai

  committed
  cc3df42

  Copy full SHA for cc3df42

• add support for cdot

  xiyuzhai

  committed
  dea968e

  Copy full SHA for dea968e

• save

  xiyuzhai

  committed
  74c9d80

  Copy full SHA for 74c9d80

• fix bug in product reduction

  xiyuzhai

  committed
  9a47152

  Copy full SHA for 9a47152

• impl miracle for VdBsqElaboratorInner

  xiyuzhai

  committed
  6f739dd

  Copy full SHA for 6f739dd

• init comm_ring; remove ring

  xiyuzhai

  committed
  2a69fda

  Copy full SHA for 2a69fda

• save

  xiyuzhai

  committed
  6f76ed0

  Copy full SHA for 6f76ed0

• save

  xiyuzhai

  committed
  976fb51

  Copy full SHA for 976fb51

• save

  xiyuzhai

  committed
  66bbb1f

  Copy full SHA for 66bbb1f

• improve term show fmt in visored-baseq-elaborator

  xiyuzhai

  committed
  a070581

  Copy full SHA for a070581

• feat: fix bug in comm_ring tactic

  xiyuzhai

  committed
  dacfe4a

  Copy full SHA for dacfe4a

• feat: pass lean side for first comm_ring test

  xiyuzhai

  committed
  1d604be

  Copy full SHA for 1d604be

• save

  xiyuzhai

  committed
  43e1adb

  Copy full SHA for 43e1adb

• fix miracle initialization and uninitialization bug

  xiyuzhai

  committed
  b0445a1

  Copy full SHA for b0445a1

• x(1+x) = x + x^2

  xiyuzhai

  committed
  45ae12d

  Copy full SHA for 45ae12d

Commits on Jan 7, 2025

• add gemini baseline

  ypwang61

  committed
  6d9f082

  Copy full SHA for 6d9f082

• add gemini

  ypwang61

  committed
  e37cb83

  Copy full SHA for e37cb83

• Merge branch 'main' of github.com:xiyuzhai/husky

  ypwang61

  committed
  ef977f5

  Copy full SHA for ef977f5

• Revert "add gemini"

  Show description for 6bf1e81
  ypwang61

  committed
  6bf1e81

  Copy full SHA for 6bf1e81

• Reapply "add gemini"

  Show description for 762dd15
  ypwang61

  committed
  762dd15

  Copy full SHA for 762dd15

• save

  xiyuzhai

  committed
  e91ee72

  Copy full SHA for e91ee72

• add miracle stage

  xiyuzhai

  committed
  3f9b13f

  Copy full SHA for 3f9b13f

• impl multinomial expansion

  xiyuzhai

  committed
  2adfa9c

  Copy full SHA for 2adfa9c

• add generalization and safe guards

  xiyuzhai

  committed
  992ff4c

  Copy full SHA for 992ff4c

• save

  xiyuzhai

  committed
  2574295

  Copy full SHA for 2574295

• improve

  xiyuzhai

  committed
  498f727

  Copy full SHA for 498f727

• improve

  xiyuzhai

  committed
  9f11355

  Copy full SHA for 9f11355

• add baselines

  ypwang61

  committed
  2362c03

  Copy full SHA for 2362c03

• (1+x)(1+x) = 1 + 2x + x^2

  xiyuzhai

  committed
  5aefa6a

  Copy full SHA for 5aefa6a

• (1+x)(1+y)=1+x+y+xy

  xiyuzhai

  committed
  a3f6552

  Copy full SHA for a3f6552

• (x+y)^2=x^2+2xy+y^2

  xiyuzhai

  committed
  79aade8

  Copy full SHA for 79aade8

• (x+y)^3=x^3+3x^2y+3xy^2+y^3

  xiyuzhai

  committed
  c999efd

  Copy full SHA for c999efd

• (x+y)^4=x^4+4x^3y+6x^2y^2+4xy^3+y^4

  xiyuzhai

  committed
  a3576e4

  Copy full SHA for a3576e4

• more

  xiyuzhai

  committed
  01673d8

  Copy full SHA for 01673d8

• (1+x^2)^2=1+2x^2+x^4

  xiyuzhai

  committed
  aafc309

  Copy full SHA for aafc309

• (x^2+y^2)^2=x^4+2x^2y^2+y^4

  xiyuzhai

  committed
  3cadbaf

  Copy full SHA for 3cadbaf

• (x^n+1)^2=x^{2n}+2x^n+1

  xiyuzhai

  committed
  24693cc

  Copy full SHA for 24693cc

• (x^n+y^n)^2=x^{2n}+2x^ny^n+y^{2n}

  xiyuzhai

  committed
  c09bc49

  Copy full SHA for c09bc49

• more

  xiyuzhai

  committed
  862c9ba

  Copy full SHA for 862c9ba

• rename num-traits to num-try

  xiyuzhai

  committed
  ef096a1

  Copy full SHA for ef096a1

• rename

  xiyuzhai

  committed
  cfcc579

  Copy full SHA for cfcc579

• rename

  xiyuzhai

  committed
  9526cd1

  Copy full SHA for 9526cd1

• use bigint

  xiyuzhai

  committed
  4948ed6

  Copy full SHA for 4948ed6

• first time processing bigint in visored

  xiyuzhai

  committed
  4ccd8f7

  Copy full SHA for 4ccd8f7

• fix: assumption should be put before term_equivalent

  xiyuzhai

  committed
  a3b83db

  Copy full SHA for a3b83db

• save

  xiyuzhai

  committed
  c32ae02

  Copy full SHA for c32ae02

• remove frac from visored mir

  xiyuzhai

  committed
  c05e08d

  Copy full SHA for c05e08d

• save

  xiyuzhai

  committed
  6ff9063

  Copy full SHA for 6ff9063

• add gemini 2

  ypwang61

  committed
  bea56a7

  Copy full SHA for bea56a7

• MiracleM in lean4

  xiyuzhai

  committed
  4612a47

  Copy full SHA for 4612a47

Commits on Jan 8, 2025

• more

  xiyuzhai

  committed
  8dc1c92

  Copy full SHA for 8dc1c92

• save

  xiyuzhai

  committed
  d3e71bf

  Copy full SHA for d3e71bf

• found bug: / in lean can be integer division

  xiyuzhai

  committed
  2c38bc7

  Copy full SHA for 2c38bc7

• add expected_ty to visored-sem-expr

  xiyuzhai

  committed
  16873ac

  Copy full SHA for 16873ac

• add expected_ty to visored-mir-expr

  xiyuzhai

  committed
  a524b63

  Copy full SHA for a524b63

• add ty coercion to lean-mir-expr

  xiyuzhai

  committed
  53ab320

  Copy full SHA for 53ab320

• add type ascription to fmt

  xiyuzhai

  committed
  dc07ba5

  Copy full SHA for dc07ba5

• save

  xiyuzhai

  committed
  15733ef

  Copy full SHA for 15733ef

• feat: add type ascription

  xiyuzhai

  committed
  01ce5af

  Copy full SHA for 01ce5af

• isolate different examples xiyuzhai-husky-lang#481

  xiyuzhai

  committed
  22d2ed0

  Copy full SHA for 22d2ed0

• feat: foldm in miracle itself, simplified

  xiyuzhai

  committed
  a03926d

  Copy full SHA for a03926d

• save

  xiyuzhai

  committed
  a84d498

  Copy full SHA for a84d498

• feat: use simplified foldm for visored ring tactic

  xiyuzhai

  committed
  a6a7418

  Copy full SHA for a6a7418

• save

  xiyuzhai

  committed
  006b572

  Copy full SHA for 006b572

• improve

  xiyuzhai

  committed
  29f739c

  Copy full SHA for 29f739c

• clean up

  xiyuzhai

  committed
  6088672

  Copy full SHA for 6088672

• rename foldm to foldm_batch

  xiyuzhai

  committed
  7c67877

  Copy full SHA for 7c67877

• save

  xiyuzhai

  committed
  1359272

  Copy full SHA for 1359272

• simplify

  xiyuzhai

  committed
  ef7a343

  Copy full SHA for ef7a343

• rename to multifold, because it's not foldm

  xiyuzhai

  committed
  714d671

  Copy full SHA for 714d671

• save

  xiyuzhai

  committed
  9e31b98

  Copy full SHA for 9e31b98

• impl call stack, xiyuzhai-husky-lang#485; init caches

  xiyuzhai

  committed
  3a28d26

  Copy full SHA for 3a28d26

• rename cache to stash

  xiyuzhai

  committed
  ffff7be

  Copy full SHA for ffff7be

• save

  xiyuzhai

  committed
  f116e7f

  Copy full SHA for f116e7f

• save

  xiyuzhai

  committed
  1e430e5

  Copy full SHA for 1e430e5

• save

  xiyuzhai

  committed
  5549556

  Copy full SHA for 5549556

• save

  xiyuzhai

  committed
  86e03ea

  Copy full SHA for 86e03ea

• save

  xiyuzhai

  committed
  0a0ce02

  Copy full SHA for 0a0ce02

• save

  xiyuzhai

  committed
  fe6947a

  Copy full SHA for fe6947a

• save

  xiyuzhai

  committed
  8f90960

  Copy full SHA for 8f90960

Commits on Jan 9, 2025

• save

  xiyuzhai

  committed
  a26d900

  Copy full SHA for a26d900

• save

  xiyuzhai

  committed
  6f77c83

  Copy full SHA for 6f77c83

• feat: foldm!!!

  xiyuzhai

  committed
  610a90f

  Copy full SHA for 610a90f

• no longer need monadic-fold

  xiyuzhai

  committed
  ab1dafc

  Copy full SHA for ab1dafc

• save

  xiyuzhai

  committed
  9dc5503

  Copy full SHA for 9dc5503

• impl litnum_equality stash

  xiyuzhai

  committed
  e3d4545

  Copy full SHA for e3d4545

• save

  xiyuzhai

  committed
  4e7457d

  Copy full SHA for 4e7457d

• add expr_equivalent

  xiyuzhai

  committed
  af8bc58

  Copy full SHA for af8bc58

• save

  xiyuzhai

  committed
  197324a

  Copy full SHA for 197324a

• save

  xiyuzhai

  committed
  669f474

  Copy full SHA for 669f474

• save

  xiyuzhai

  committed
  3cf8522

  Copy full SHA for 3cf8522

• save

  xiyuzhai

  committed
  094104d

  Copy full SHA for 094104d

• impl debug for elaborator

  xiyuzhai

  committed
  1614321

  Copy full SHA for 1614321

• save

  xiyuzhai

  committed
  8a6fbe6

  Copy full SHA for 8a6fbe6

• save

  xiyuzhai

  committed
  e15bac6

  Copy full SHA for e15bac6

• save

  xiyuzhai

  committed
  2d16adf

  Copy full SHA for 2d16adf

• save

  xiyuzhai

  committed
  1e2b968

  Copy full SHA for 1e2b968

• feat: let assigned

  xiyuzhai

  committed
  188f510

  Copy full SHA for 188f510

• improve lean-mir-expr fmt

  xiyuzhai

  committed
  0bf4927

  Copy full SHA for 0bf4927

• quality of life update: improve lean parameter transpilation

  xiyuzhai

  committed
  6426081

  Copy full SHA for 6426081