The option on GoalTacticResult.goals? is redundant #24

New Issue

aniva · 2023-10-28T16:37:48-07:00

aniva commented

2023-10-28 16:37:48 -07:00

It always gets filled:

-- Pantograph.lean
        return .ok {
          nextStateId? := .some nextStateId,
          goals? := .some goals,
        }

It always gets filled: ```lean -- Pantograph.lean return .ok { nextStateId? := .some nextStateId, goals? := .some goals, } ```

aniva added this to the 0.3 milestone 2023-10-28 16:37:48 -07:00

aniva added the

category

optimization

label 2023-10-28 16:37:48 -07:00

aniva self-assigned this 2023-10-28 16:37:48 -07:00

aniva commented

2023-11-06 11:14:46 -08:00

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. However this requires non trivial state tracking machinery which should probably be implemented in the client.

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. However this requires non trivial state tracking machinery which should probably be implemented in the client.

aniva modified the milestone from 0.3 to 0.2.10

2023-11-30 01:04:28 -08:00

aniva closed this issue

2024-01-16 14:20:31 -08:00

Sign in to join this conversation.