Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
radeusgd committed Feb 27, 2025
1 parent a283f02 commit 344f44d
Show file tree
Hide file tree
Showing 3 changed files with 18 additions and 1 deletion.
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
private

import project.Column.Column
import project.Table.Table
import project.Refined_Types.Numeric_Column.Numeric_Column

from project.Internal.Type_Refinements.Single_Column_Table_Conversions import all
from project.Internal.Type_Refinements.Typed_Column_Conversions import all

## This conversion is internal and should never be exported.
Numeric_Column.from (that : Table) =
Numeric_Column.from (Column.from that)
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import project.Refined_Types.Numeric_Column.Numeric_Column
import project.Table.Table
import project.Value_Type.Value_Type
from project.Internal.Type_Refinements.Single_Column_Table_Conversions import all
from project.Internal.Type_Refinements.Single_Column_Typed_Table_Conversions import all
from project.Internal.Type_Refinements.Column_Refinements import is_single_value

refine_table (table : Table) =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -53,5 +53,9 @@ add_numeric_columns_specs suite_builder setup =
signum_column.to_vector . should_equal [-1, 0, 0, 1, 1]

group_builder.specify "a single value column can also be Numeric_Column" <|
column = table_builder [["X", [1]]] . at "X"
table = table_builder [["X", [1]]]
column = table . at "X"
column:Numeric_Column

# But a single column table can also be converted
table:Numeric_Column

0 comments on commit 344f44d

Please sign in to comment.