Leni Aniva aniva
0 Followers · 1 Following
  • Stanford University Centaur Group
  • https://leni.sh

  • Admin of this website

  • Joined on 2023-08-21
Repositories
10
 Projects Packages Public Activity Starred Repositories
2
aniva pushed to misc/cleanup at aniva/Pantograph 2023-11-06 11:39:29 -08:00
f5ed87f740 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev
8dd994d1ca bug: Fix quote escape problem
d87217c6bb feat: Print metavariable name in goal
796f0d8336 Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
e5acd4b26c fix: Sanitize name in universe levels
Compare 37 commits »
aniva commented on issue aniva/Pantograph#24 2023-11-06 11:14:46 -08:00
The option on GoalTacticResult.goals? is redundant

I don't think this is a problem. We can repurpose this so that .none means all goals are solved and there are no couplings, while .some [] means all goals are solved but some couplings exist.…

aniva created pull request aniva/Pantograph#28 2023-11-06 11:12:35 -08:00
WIP: Proof tracing from theorem library
aniva created branch library/trace in aniva/Pantograph 2023-11-06 11:10:36 -08:00
aniva pushed to library/trace at aniva/Pantograph 2023-11-06 11:10:36 -08:00
aniva pushed to goal/continuation at aniva/Pantograph 2023-11-06 11:04:42 -08:00
a7aeb03b43 chore: Update documentation
aniva pushed to goal/continuation at aniva/Pantograph 2023-11-06 10:45:41 -08:00
dbace9f2d5 fix: Use Lean's built in name parser
aniva pushed to goal/continuation at aniva/Pantograph 2023-11-04 15:54:41 -07:00
782ce38c87 chore: Version bump to 0.2.8
d809a960f9 feat: Goal continuation fails if target has goals
db706070ad feat: Add goal.continue command
754fb69cff feat: Partial state continuation
dc2cc5be77 test: Separate mvar coupling tests
Compare 5 commits »
aniva created pull request aniva/Pantograph#27 2023-11-03 23:43:44 -07:00
feat: Allow selective continuation of goals
aniva created branch goal/continuation in aniva/Pantograph 2023-11-03 23:43:16 -07:00
aniva pushed to goal/continuation at aniva/Pantograph 2023-11-03 23:43:16 -07:00
aniva pushed tag v0.2.7 to aniva/Pantograph 2023-10-30 14:49:38 -07:00
aniva pushed tag 0.1 to aniva/Pantograph 2023-10-30 14:49:23 -07:00
aniva pushed to dev at aniva/Pantograph 2023-10-30 14:47:44 -07:00
f5ed87f740 Merge pull request 'feat: Minor updates to serialization' (#26) from io/serial into dev
8dd994d1ca bug: Fix quote escape problem
d87217c6bb feat: Print metavariable name in goal
Compare 3 commits »
aniva merged pull request aniva/Pantograph#26 2023-10-30 14:47:42 -07:00
feat: Minor updates to serialization
aniva created pull request aniva/Pantograph#26 2023-10-30 14:47:01 -07:00
Minor updates to serialization
aniva pushed to io/serial at aniva/Pantograph 2023-10-30 14:45:49 -07:00
8dd994d1ca bug: Fix quote escape problem
aniva pushed to io/serial at aniva/Pantograph 2023-10-30 14:44:15 -07:00
d87217c6bb feat: Print metavariable name in goal
796f0d8336 Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
Compare 2 commits »
aniva commented on issue aniva/Pantograph#22 2023-10-29 13:08:46 -07:00
Use special handling to print compound names

Solved #25

aniva closed issue aniva/Pantograph#22 2023-10-29 13:08:46 -07:00
Use special handling to print compound names