Code

remove lean output#500

Code

Merged

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

+9,093-2,279

Commits

Commits on Jan 9, 2025

• save

  xiyuzhai

  committed
  80dfc7e

  Copy full SHA for 80dfc7e

• save

  xiyuzhai

  committed
  8bc7cdc

  Copy full SHA for 8bc7cdc

Commits on Jan 10, 2025

• save

  xiyuzhai

  committed
  40b84a6

  Copy full SHA for 40b84a6

• feat: perfect rust monad works

  xiyuzhai

  committed
  9814620

  Copy full SHA for 9814620

• save

  xiyuzhai

  committed
  5917440

  Copy full SHA for 5917440

• save

  xiyuzhai

  committed
  9032ebf

  Copy full SHA for 9032ebf

• save

  xiyuzhai

  committed
  24b5a2a

  Copy full SHA for 24b5a2a

• unify_elabm macro

  xiyuzhai

  committed
  a3559e2

  Copy full SHA for a3559e2

• feat: move miracle to the top level

  xiyuzhai

  committed
  3936732

  Copy full SHA for 3936732

• Merge branch 'xiyuzhai-husky-lang:main' into main

  xiyuzhai

  authored
  cc4bc91

  Copy full SHA for cc4bc91

• save

  xiyuzhai

  committed
  0af0412

  Copy full SHA for 0af0412

• save

  xiyuzhai

  committed
  fc5d743

  Copy full SHA for fc5d743

• Merge remote-tracking branch 'refs/remotes/origin/main'

  xiyuzhai

  committed
  bd3d096

  Copy full SHA for bd3d096

• save

  xiyuzhai

  committed
  92b9302

  Copy full SHA for 92b9302

• save

  xiyuzhai

  committed
  9f1ef75

  Copy full SHA for 9f1ef75

• save

  xiyuzhai

  committed
  b06ca51

  Copy full SHA for b06ca51

• save

  xiyuzhai

  committed
  778f936

  Copy full SHA for 778f936

• save

  xiyuzhai

  committed
  a7e580f

  Copy full SHA for a7e580f

• save

  xiyuzhai

  committed
  3aa4922

  Copy full SHA for 3aa4922

• save

  xiyuzhai

  committed
  697c836

  Copy full SHA for 697c836

• save

  xiyuzhai

  committed
  d61a6ba

  Copy full SHA for d61a6ba

• save

  xiyuzhai

  committed
  6e29871

  Copy full SHA for 6e29871

• save

  xiyuzhai

  committed
  2ba72f7

  Copy full SHA for 2ba72f7

• feat: visored proved x > 0 if x = 1.

  xiyuzhai

  committed
  725c5d6

  Copy full SHA for 725c5d6

• ad hoc implementation of litnum_reduce lean transpilation

  xiyuzhai

  committed
  244039a

  Copy full SHA for 244039a

Commits on Jan 11, 2025

• more litnum reductions

  xiyuzhai

  committed
  9184013

  Copy full SHA for 9184013

• add some elementary inequalities

  xiyuzhai

  committed
  980fe11

  Copy full SHA for 980fe11

• replace expr_equivalent with old_main_hypothesis, xiyuzhai-husky-lang#488

  xiyuzhai

  committed
  edeb3ec

  Copy full SHA for edeb3ec

• fix unnecessary new line

  xiyuzhai

  committed
  d98aa2b

  Copy full SHA for d98aa2b

• save

  xiyuzhai

  committed
  b4054d2

  Copy full SHA for b4054d2

• save

  xiyuzhai

  committed
  9f41fe3

  Copy full SHA for 9f41fe3

• save

  xiyuzhai

  committed
  e76a1a0

  Copy full SHA for e76a1a0

• save

  xiyuzhai

  committed
  dcbeda1

  Copy full SHA for dcbeda1

• feat: if x>1, then x>0

  xiyuzhai

  committed
  dc1d893

  Copy full SHA for dc1d893

• fix bug: too restrictive in litnum bound new key

  xiyuzhai

  committed
  f312b2b

  Copy full SHA for f312b2b

• fix bug in finalizing litnum bound

  xiyuzhai

  committed
  65cdc81

  Copy full SHA for 65cdc81

• save

  xiyuzhai

  committed
  6094991

  Copy full SHA for 6094991

• save

  xiyuzhai

  committed
  7aebbfb

  Copy full SHA for 7aebbfb

• save

  xiyuzhai

  committed
  1ad518f

  Copy full SHA for 1ad518f

• save

  xiyuzhai

  committed
  e975398

  Copy full SHA for e975398

• save

  xiyuzhai

  committed
  34cabde

  Copy full SHA for 34cabde

• save

  xiyuzhai

  committed
  5a1e255

  Copy full SHA for 5a1e255

• bug found

  xiyuzhai

  committed
  90d673f

  Copy full SHA for 90d673f

• fix bug

  xiyuzhai

  committed
  0dab4ad

  Copy full SHA for 0dab4ad

• save

  xiyuzhai

  committed
  e3a8ba3

  Copy full SHA for e3a8ba3

• save

  xiyuzhai

  committed
  987ec75

  Copy full SHA for 987ec75

• save

  xiyuzhai

  committed
  62fee09

  Copy full SHA for 62fee09

• more tests

  xiyuzhai

  committed
  9434175

  Copy full SHA for 9434175

• save

  xiyuzhai

  committed
  eb5169c

  Copy full SHA for eb5169c

• fix bug in split

  xiyuzhai

  committed
  036d684

  Copy full SHA for 036d684

• more tests

  xiyuzhai

  committed
  8fd0166

  Copy full SHA for 8fd0166

• save

  xiyuzhai

  committed
  ece5a1d

  Copy full SHA for ece5a1d

Commits on Jan 12, 2025

• save

  xiyuzhai

  committed
  95cf6d2

  Copy full SHA for 95cf6d2

• save

  xiyuzhai

  committed
  0ff04d0

  Copy full SHA for 0ff04d0

• save

  xiyuzhai

  committed
  da3005b

  Copy full SHA for da3005b

• save

  xiyuzhai

  committed
  b15b59e

  Copy full SHA for b15b59e

• save

  xiyuzhai

  committed
  063e315

  Copy full SHA for 063e315

• save

  xiyuzhai

  committed
  252d351

  Copy full SHA for 252d351

• save

  xiyuzhai

  committed
  6635563

  Copy full SHA for 6635563

• feat: overhaul term system in visored-baseq-elaborator

  xiyuzhai

  committed
  e1e9d23

  Copy full SHA for e1e9d23

• remove VdBsqProductBase::Sum, xiyuzhai-husky-lang#493

  xiyuzhai

  committed
  ee1d3d5

  Copy full SHA for ee1d3d5

• save

  xiyuzhai

  committed
  11e13d4

  Copy full SHA for 11e13d4

• intro kurapika tactic

  xiyuzhai

  committed
  3d2ced7

  Copy full SHA for 3d2ced7

• make lean transpilation of nontrivial chain pass

  xiyuzhai

  committed
  28a1781

  Copy full SHA for 28a1781

• update visored lean transpilation

  xiyuzhai

  committed
  94c1558

  Copy full SHA for 94c1558

• unify dev and test profiles

  xiyuzhai

  committed
  4dfabfd

  Copy full SHA for 4dfabfd

• improve regularization prompt

  xiyuzhai

  committed
  7501839

  Copy full SHA for 7501839

• use header instead of package for lean4

  xiyuzhai

  committed
  42e7f52

  Copy full SHA for 42e7f52

• save

  xiyuzhai

  committed
  b9a2e2a

  Copy full SHA for b9a2e2a

• save

  xiyuzhai

  committed
  b9e3dfe

  Copy full SHA for b9e3dfe

• save

  xiyuzhai

  committed
  46f3bfb

  Copy full SHA for 46f3bfb

• save

  xiyuzhai

  committed
  8ecf5be

  Copy full SHA for 8ecf5be

• save

  xiyuzhai

  committed
  42fef68

  Copy full SHA for 42fef68

• met some technical issues with mir show stmt

  xiyuzhai

  committed
  7b6e1f7

  Copy full SHA for 7b6e1f7

Commits on Jan 13, 2025

• save

  xiyuzhai

  committed
  c60ea7c

  Copy full SHA for c60ea7c

• save

  xiyuzhai

  committed
  802397c

  Copy full SHA for 802397c

• save

  xiyuzhai

  committed
  1c42f42

  Copy full SHA for 1c42f42

• save

  xiyuzhai

  committed
  9741bf8

  Copy full SHA for 9741bf8

• translate in_set to true instead of sorry

  xiyuzhai

  committed
  2a8a3b3

  Copy full SHA for 2a8a3b3

• batch 2 example 8; impl support for div binary opr

  xiyuzhai

  committed
  6e7c267

  Copy full SHA for 6e7c267

• batch 1 example 9

  xiyuzhai

  committed
  ce4e1f5

  Copy full SHA for ce4e1f5

• save

  xiyuzhai

  committed
  904cd49

  Copy full SHA for 904cd49

• save

  xiyuzhai

  committed
  4b79508

  Copy full SHA for 4b79508

• save

  xiyuzhai

  committed
  4d662f0

  Copy full SHA for 4d662f0

• save

  xiyuzhai

  committed
  216ffbb

  Copy full SHA for 216ffbb

• save

  xiyuzhai

  committed
  8e29270

  Copy full SHA for 8e29270

• save

  xiyuzhai

  committed
  261e999

  Copy full SHA for 261e999

• save

  xiyuzhai

  committed
  496b64e

  Copy full SHA for 496b64e

• feat: integrate visored-baseq-elaborator into visored-pipeline

  xiyuzhai

  committed
  9b045f4

  Copy full SHA for 9b045f4

Commits on Jan 14, 2025

• update expect

  xiyuzhai

  committed
  3aa36c6

  Copy full SHA for 3aa36c6