Safe HaskellNone

MAlonzo.Code.Algebra.Solver.Ring

Documentation

d_Carrier_66 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> () Source #

d__'42'__72 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'42'__72 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'43'__74 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny Source #

du__'43'__74 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d__'8776'__76 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny -> () Source #

d_'45'__160 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny Source #

du_'45'__160 :: T_AlmostCommutativeRing_178 -> AgdaAny -> AgdaAny Source #

d_0'35'_168 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny Source #

du_0'35'_168 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_1'35'_170 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny Source #

du_1'35'_170 :: T_AlmostCommutativeRing_178 -> AgdaAny Source #

d_Carrier_172 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> () Source #

d_'10214'_'10215'_310 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny Source #

du_'10214'_'10215'_310 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> AgdaAny -> AgdaAny Source #

d__'94'__314 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> AgdaAny -> Integer -> AgdaAny Source #

du__'94'__314 :: T_AlmostCommutativeRing_178 -> AgdaAny -> Integer -> AgdaAny Source #

d_Op_348 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> () Source #

data T_Op_348 Source #

Constructors

C_'91''43''93'_350 
C_'91''42''93'_352 

d_Polynomial_356 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_Polynomial_356 Source #

Constructors

C_op_366 T_Op_348 T_Polynomial_356 T_Polynomial_356 
C_con_370 AgdaAny 
C_var_374 T_Fin_6 
C__'58''94'__380 T_Polynomial_356 Integer 
C_'58''45'__384 T_Polynomial_356 

d__'58''43'__388 :: T_Polynomial_356 -> T_Polynomial_356 -> T_Polynomial_356 Source #

d__'58''42'__392 :: T_Polynomial_356 -> T_Polynomial_356 -> T_Polynomial_356 Source #

d__'58''45'__396 :: T_Polynomial_356 -> T_Polynomial_356 -> T_Polynomial_356 Source #

d__'58''215'__404 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> Integer -> T_Polynomial_356 -> T_Polynomial_356 Source #

du__'58''215'__404 :: T_RawRing_2558 -> Integer -> T_Polynomial_356 -> T_Polynomial_356 Source #

d_sem_412 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> T_Op_348 -> AgdaAny -> AgdaAny -> AgdaAny Source #

du_sem_412 :: T_AlmostCommutativeRing_178 -> T_Op_348 -> AgdaAny -> AgdaAny -> AgdaAny Source #

d_'10214'_'10215'_416 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Polynomial_356 -> T_Vec_28 -> AgdaAny Source #

du_'10214'_'10215'_416 :: T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> T_Polynomial_356 -> T_Vec_28 -> AgdaAny Source #

d_HNF_444 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_HNF_444 Source #

Constructors

C_'8709'_450 
C__'42'x'43'__454 T_HNF_444 T_Normal_446 

d_Normal_446 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> () Source #

data T_Normal_446 Source #

Constructors

C_con_456 AgdaAny 
C_poly_460 T_HNF_444 

d_'10214'_'10215'H_464 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Vec_28 -> AgdaAny Source #

d_'10214'_'10215'N_468 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Vec_28 -> AgdaAny Source #

d__'8776'H__486 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

data T__'8776'H__486 Source #

Constructors

C_'8709'_494 
C__'42'x'43'__506 T__'8776'H__486 T__'8776'N__490 

d__'8776'N__490 :: p1 -> p2 -> p3 -> p4 -> p5 -> p6 -> p7 -> p8 -> p9 -> p10 -> p11 -> () Source #

data T__'8776'N__490 Source #

Constructors

C_con_512 AgdaAny 
C_poly_520 T__'8776'H__486 

d__'8799'H__524 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> Maybe T__'8776'H__486 Source #

d__'8799'N__528 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> Maybe T__'8776'N__490 Source #

d_'10214'_'10215'H'45'cong_614 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T__'8776'H__486 -> T_Vec_28 -> AgdaAny Source #

d_'10214'_'10215'N'45'cong_624 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> T__'8776'N__490 -> T_Vec_28 -> AgdaAny Source #

d_0H_642 :: T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 Source #

du_0H_642 :: T_HNF_444 Source #

d_0N_646 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 Source #

du_0N_646 :: T_RawRing_2558 -> Integer -> T_Normal_446 Source #

d_1H_652 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 Source #

d_1N_656 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 Source #

d__'42'x'43'HN__664 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Normal_446 -> T_HNF_444 Source #

d__'43'H__686 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T_HNF_444 Source #

d__'43'N__690 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> T_Normal_446 Source #

d__'42'x'43'H__714 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T_HNF_444 Source #

d__'42'NH__728 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_HNF_444 -> T_HNF_444 Source #

d__'42'HN__732 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Normal_446 -> T_HNF_444 Source #

d__'42'H__736 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T_HNF_444 Source #

d__'42'N__740 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> T_Normal_446 Source #

d__'94'N__812 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> Integer -> T_Normal_446 Source #

d_'45'H__822 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 Source #

d_'45'N__826 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 Source #

d_normalise'45'con_836 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> AgdaAny -> T_Normal_446 Source #

d_normalise'45'var_846 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Fin_6 -> T_Normal_446 Source #

d_normalise_852 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Polynomial_356 -> T_Normal_446 Source #

d_'10214'_'10215''8595'_874 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Polynomial_356 -> T_Vec_28 -> AgdaAny Source #

d_0N'45'homo_884 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Vec_28 -> AgdaAny Source #

d_0'8776''10214'0'10215'_896 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T__'8776'N__490 -> T_Vec_28 -> AgdaAny Source #

d_1N'45'homo_908 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Vec_28 -> AgdaAny Source #

d_'42'x'43'HN'8776''42'x'43'_922 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Normal_446 -> T_Vec_28 -> AgdaAny Source #

d_'8709''42'x'43'HN'45'homo_964 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> AgdaAny -> T_Vec_28 -> AgdaAny Source #

d_'43'H'45'homo_998 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T_Vec_28 -> AgdaAny Source #

d_'43'N'45'homo_1008 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> T_Vec_28 -> AgdaAny Source #

d_'42'x'43'H'45'homo_1052 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> AgdaAny -> T_Vec_28 -> AgdaAny Source #

d_'42'NH'45'homo_1082 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_HNF_444 -> AgdaAny -> T_Vec_28 -> AgdaAny Source #

d_'42'HN'45'homo_1094 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Normal_446 -> AgdaAny -> T_Vec_28 -> AgdaAny Source #

d_'42'H'45'homo_1104 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_HNF_444 -> T_Vec_28 -> AgdaAny Source #

d_'42'N'45'homo_1114 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Normal_446 -> T_Vec_28 -> AgdaAny Source #

d_'94'N'45'homo_1240 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> Integer -> T_Vec_28 -> AgdaAny Source #

d_'45'H'8255''45'homo_1258 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_HNF_444 -> T_Vec_28 -> AgdaAny Source #

d_'45'N'8255''45'homo_1266 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Normal_446 -> T_Vec_28 -> AgdaAny Source #

d_correct'45'con_1286 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> AgdaAny -> T_Vec_28 -> AgdaAny Source #

d_correct'45'var_1302 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Fin_6 -> T_Vec_28 -> AgdaAny Source #

d_correct_1320 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Polynomial_356 -> T_Vec_28 -> AgdaAny Source #

d__'8860'__1354 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Polynomial_356 -> T_Polynomial_356 -> T_Σ_14 Source #

du__'8860'__1354 :: Integer -> T_Polynomial_356 -> T_Polynomial_356 -> T_Σ_14 Source #

d_prove_1356 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> T_Vec_28 -> T_Polynomial_356 -> T_Polynomial_356 -> AgdaAny -> AgdaAny Source #

d_solve_1358 :: T_Level_14 -> T_Level_14 -> T_Level_14 -> T_Level_14 -> T_RawRing_2558 -> T_AlmostCommutativeRing_178 -> T__'45'Raw'45'AlmostCommutative'10230'__358 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny) -> Integer -> AgdaAny -> AgdaAny -> AgdaAny Source #