mirror of
https://gitlab.com/sheaf/metabrush.git
synced 2024-11-23 15:34:06 +00:00
cleanups
This commit is contained in:
parent
2bae92dc5e
commit
9ff25a25aa
|
@ -135,7 +135,7 @@ common extras
|
||||||
, stm
|
, stm
|
||||||
^>= 2.5.0.0
|
^>= 2.5.0.0
|
||||||
, text
|
, text
|
||||||
^>= 2.1.1
|
>= 2.0 && < 3
|
||||||
, unordered-containers
|
, unordered-containers
|
||||||
>= 0.2.11 && < 0.3
|
>= 0.2.11 && < 0.3
|
||||||
, waargonaut
|
, waargonaut
|
||||||
|
@ -151,7 +151,7 @@ common gtk
|
||||||
, gi-gdk
|
, gi-gdk
|
||||||
>= 4.0.2 && < 4.1
|
>= 4.0.2 && < 4.1
|
||||||
, gi-gio
|
, gi-gio
|
||||||
>= 2.0.27 && < 2.1
|
>= 2.0.34 && < 2.1
|
||||||
, gi-glib
|
, gi-glib
|
||||||
>= 2.0.23 && < 2.1
|
>= 2.0.23 && < 2.1
|
||||||
, gi-gobject
|
, gi-gobject
|
||||||
|
|
|
@ -38,11 +38,13 @@ class
|
||||||
( Module ( I i Double ) ( T ( I i u ) )
|
( Module ( I i Double ) ( T ( I i u ) )
|
||||||
, HasChainRule ( I i Double ) k ( I i u )
|
, HasChainRule ( I i Double ) k ( I i u )
|
||||||
, Traversable ( D k u )
|
, Traversable ( D k u )
|
||||||
|
, Representable ( I i Double ) ( I i u )
|
||||||
) => Differentiable k i u
|
) => Differentiable k i u
|
||||||
instance
|
instance
|
||||||
( Module ( I i Double ) ( T ( I i u ) )
|
( Module ( I i Double ) ( T ( I i u ) )
|
||||||
, HasChainRule ( I i Double ) k ( I i u )
|
, HasChainRule ( I i Double ) k ( I i u )
|
||||||
, Traversable ( D k u )
|
, Traversable ( D k u )
|
||||||
|
, Representable ( I i Double ) ( I i u )
|
||||||
) => Differentiable k i u
|
) => Differentiable k i u
|
||||||
|
|
||||||
type DiffInterp :: Nat -> k -> Nat -> Constraint
|
type DiffInterp :: Nat -> k -> Nat -> Constraint
|
||||||
|
@ -55,7 +57,6 @@ class
|
||||||
, Transcendental ( D k u ( I i Double ) )
|
, Transcendental ( D k u ( I i Double ) )
|
||||||
, Applicative ( D k u )
|
, Applicative ( D k u )
|
||||||
, Representable ( I i Double ) ( I i u )
|
, Representable ( I i Double ) ( I i u )
|
||||||
, RepDim ( I i u ) ~ RepDim u
|
|
||||||
) => DiffInterp k i u
|
) => DiffInterp k i u
|
||||||
instance
|
instance
|
||||||
( Differentiable k i u
|
( Differentiable k i u
|
||||||
|
@ -66,5 +67,4 @@ instance
|
||||||
, Transcendental ( D k u ( I i Double ) )
|
, Transcendental ( D k u ( I i Double ) )
|
||||||
, Applicative ( D k u )
|
, Applicative ( D k u )
|
||||||
, Representable ( I i Double ) ( I i u )
|
, Representable ( I i Double ) ( I i u )
|
||||||
, RepDim ( I i u ) ~ RepDim u
|
|
||||||
) => DiffInterp k i u
|
) => DiffInterp k i u
|
||||||
|
|
|
@ -120,7 +120,7 @@ import MetaBrush.Document
|
||||||
import {-# SOURCE #-} MetaBrush.Document.Update
|
import {-# SOURCE #-} MetaBrush.Document.Update
|
||||||
( DocChange(..) )
|
( DocChange(..) )
|
||||||
import MetaBrush.Records
|
import MetaBrush.Records
|
||||||
( Record
|
( Record(..)
|
||||||
, Intersection(..), intersect
|
, Intersection(..), intersect
|
||||||
)
|
)
|
||||||
import MetaBrush.Unique
|
import MetaBrush.Unique
|
||||||
|
@ -890,7 +890,7 @@ applyBrushWidgetAction pressingCtrl c mbPrevAction doc@( Document { zoomFactor }
|
||||||
| otherwise
|
| otherwise
|
||||||
-> case intersect @pointFields @brushFields of
|
-> case intersect @pointFields @brushFields of
|
||||||
Intersection { inject1 = injectUsedParams, inject2 = updateBrushParams, project1 = ptParamsToUsedParams, project2 = brushParamsToUsedParams } -> do
|
Intersection { inject1 = injectUsedParams, inject2 = updateBrushParams, project1 = ptParamsToUsedParams, project2 = brushParamsToUsedParams } -> do
|
||||||
let embedUsedParams = updateBrushParams ( defaultParams $ brushFunction brush )
|
let embedUsedParams = updateBrushParams ( MkR $ defaultParams $ brushFunction brush )
|
||||||
toBrushParams = embedUsedParams . ptParamsToUsedParams
|
toBrushParams = embedUsedParams . ptParamsToUsedParams
|
||||||
updatePointParams brushParams' ptParams = injectUsedParams ptParams ( brushParamsToUsedParams brushParams' )
|
updatePointParams brushParams' ptParams = injectUsedParams ptParams ( brushParamsToUsedParams brushParams' )
|
||||||
spline' <- updateSpline brush toBrushParams updatePointParams strokeUnique spline0
|
spline' <- updateSpline brush toBrushParams updatePointParams strokeUnique spline0
|
||||||
|
|
|
@ -11,6 +11,8 @@ import Control.Monad
|
||||||
( guard, when, unless )
|
( guard, when, unless )
|
||||||
import Control.Monad.ST
|
import Control.Monad.ST
|
||||||
( RealWorld, ST )
|
( RealWorld, ST )
|
||||||
|
import Data.Coerce
|
||||||
|
( coerce )
|
||||||
import Data.Fixed
|
import Data.Fixed
|
||||||
( mod' )
|
( mod' )
|
||||||
import Data.Foldable
|
import Data.Foldable
|
||||||
|
@ -319,12 +321,12 @@ strokeRenderData rootAlgo mbCuspOptions fitParams
|
||||||
{ inject2
|
{ inject2
|
||||||
, project1 = toUsedParams :: Record pointFields -> Record usedFields }
|
, project1 = toUsedParams :: Record pointFields -> Record usedFields }
|
||||||
-> do
|
-> do
|
||||||
let embedUsedParams = inject2 brush_defaults
|
let embedUsedParams = inject2 $ MkR brush_defaults
|
||||||
|
|
||||||
-- Compute the outline using the brush function.
|
-- Compute the outline using the brush function.
|
||||||
( outline, fitPts, cusps ) <-
|
( outline, fitPts, cusps ) <-
|
||||||
computeStrokeOutline @clo rootAlgo mbCuspOptions fitParams
|
computeStrokeOutline @clo rootAlgo mbCuspOptions fitParams
|
||||||
( toUsedParams . brushParams ) embedUsedParams
|
( coerce toUsedParams . brushParams ) ( coerce embedUsedParams )
|
||||||
brush spline
|
brush spline
|
||||||
pure $
|
pure $
|
||||||
StrokeWithOutlineRenderData
|
StrokeWithOutlineRenderData
|
||||||
|
@ -332,7 +334,7 @@ strokeRenderData rootAlgo mbCuspOptions fitParams
|
||||||
, strokeOutlineData = ( outline, fitPts, cusps )
|
, strokeOutlineData = ( outline, fitPts, cusps )
|
||||||
, strokeBrushFunction =
|
, strokeBrushFunction =
|
||||||
\ params ->
|
\ params ->
|
||||||
let brushParams = embedUsedParams $ toUsedParams params
|
let MkR brushParams = embedUsedParams $ toUsedParams params
|
||||||
shape = fun @Double brushBaseShape brushParams
|
shape = fun @Double brushBaseShape brushParams
|
||||||
-- TODO: remove this logic which is duplicated
|
-- TODO: remove this logic which is duplicated
|
||||||
-- from elsewhere. The type should make it
|
-- from elsewhere. The type should make it
|
||||||
|
|
|
@ -41,8 +41,6 @@ import MetaBrush.Brush
|
||||||
( NamedBrush(..), SomeBrush(..), WithParams(..) )
|
( NamedBrush(..), SomeBrush(..), WithParams(..) )
|
||||||
import qualified MetaBrush.Brush.Widget as Brush
|
import qualified MetaBrush.Brush.Widget as Brush
|
||||||
( Widget(..) )
|
( Widget(..) )
|
||||||
import MetaBrush.Records
|
|
||||||
( Record(MkR) )
|
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
|
@ -69,8 +67,7 @@ circle =
|
||||||
, brushWidget = Brush.SquareWidget
|
, brushWidget = Brush.SquareWidget
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
deflts :: Record CircleBrushFields
|
deflts = ℝ1 1
|
||||||
deflts = MkR ( ℝ1 1 )
|
|
||||||
{-# INLINE circle #-}
|
{-# INLINE circle #-}
|
||||||
|
|
||||||
type EllipseBrushFields = '[ "a", "b", "phi" ]
|
type EllipseBrushFields = '[ "a", "b", "phi" ]
|
||||||
|
@ -84,8 +81,7 @@ ellipse =
|
||||||
, brushWidget = Brush.RotatableRectangleWidget
|
, brushWidget = Brush.RotatableRectangleWidget
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
deflts :: Record EllipseBrushFields
|
deflts = ℝ3 1 1 0
|
||||||
deflts = MkR ( ℝ3 1 1 0 )
|
|
||||||
{-# INLINE ellipse #-}
|
{-# INLINE ellipse #-}
|
||||||
|
|
||||||
type TearDropBrushFields = '[ "w", "h", "phi" ]
|
type TearDropBrushFields = '[ "w", "h", "phi" ]
|
||||||
|
@ -98,6 +94,5 @@ tearDrop =
|
||||||
, brushWidget = Brush.RotatableRectangleWidget
|
, brushWidget = Brush.RotatableRectangleWidget
|
||||||
}
|
}
|
||||||
where
|
where
|
||||||
deflts :: Record TearDropBrushFields
|
deflts = ℝ3 1 2.25 0
|
||||||
deflts = MkR ( ℝ3 1 2.25 0 )
|
|
||||||
{-# INLINE tearDrop #-}
|
{-# INLINE tearDrop #-}
|
||||||
|
|
|
@ -24,6 +24,8 @@ import GHC.TypeLits
|
||||||
( Symbol, someSymbolVal
|
( Symbol, someSymbolVal
|
||||||
, SomeSymbol(..)
|
, SomeSymbol(..)
|
||||||
)
|
)
|
||||||
|
import GHC.TypeNats
|
||||||
|
( Nat )
|
||||||
|
|
||||||
-- deepseq
|
-- deepseq
|
||||||
import Control.DeepSeq
|
import Control.DeepSeq
|
||||||
|
@ -59,11 +61,11 @@ import MetaBrush.Serialisable
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
-- | A brush, with default parameter values.
|
-- | A brush, with default parameter values.
|
||||||
type WithParams :: Type -> Type
|
type WithParams :: Nat -> Type
|
||||||
data WithParams params =
|
data WithParams nbParams =
|
||||||
WithParams
|
WithParams
|
||||||
{ defaultParams :: params
|
{ defaultParams :: ℝ nbParams
|
||||||
, withParams :: Brush params
|
, withParams :: Brush nbParams
|
||||||
}
|
}
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
@ -71,7 +73,7 @@ data WithParams params =
|
||||||
-- | A brush function: a function from a record of parameters to a closed spline.
|
-- | A brush function: a function from a record of parameters to a closed spline.
|
||||||
type BrushFunction :: [ Symbol ] -> Type
|
type BrushFunction :: [ Symbol ] -> Type
|
||||||
type BrushFunction brushFields =
|
type BrushFunction brushFields =
|
||||||
WithParams ( Record brushFields )
|
WithParams ( Length brushFields )
|
||||||
|
|
||||||
type NamedBrush :: [ Symbol ] -> Type
|
type NamedBrush :: [ Symbol ] -> Type
|
||||||
data NamedBrush brushFields where
|
data NamedBrush brushFields where
|
||||||
|
@ -79,8 +81,9 @@ data NamedBrush brushFields where
|
||||||
:: forall brushFields
|
:: forall brushFields
|
||||||
. ( KnownSymbols brushFields
|
. ( KnownSymbols brushFields
|
||||||
, Representable Double ( ℝ ( Length brushFields ) )
|
, Representable Double ( ℝ ( Length brushFields ) )
|
||||||
, DiffInterp 2 () ( ℝ ( Length brushFields ) )
|
, DiffInterp 2 ℝ ( Length brushFields )
|
||||||
, DiffInterp 3 𝕀 ( ℝ ( Length brushFields ) )
|
, DiffInterp 3 𝕀 ( Length brushFields )
|
||||||
|
, Show ( ℝ ( Length brushFields ) )
|
||||||
)
|
)
|
||||||
=> { brushName :: !Text
|
=> { brushName :: !Text
|
||||||
, brushFunction :: !( BrushFunction brushFields )
|
, brushFunction :: !( BrushFunction brushFields )
|
||||||
|
@ -118,19 +121,23 @@ type PointFields :: [ Symbol ] -> Constraint
|
||||||
class ( KnownSymbols pointFields, Typeable pointFields
|
class ( KnownSymbols pointFields, Typeable pointFields
|
||||||
, Serialisable ( Record pointFields )
|
, Serialisable ( Record pointFields )
|
||||||
, Show ( Record pointFields )
|
, Show ( Record pointFields )
|
||||||
|
, Show ( ℝ ( Length pointFields ) )
|
||||||
, NFData ( Record pointFields )
|
, NFData ( Record pointFields )
|
||||||
, Representable Double ( ℝ ( Length pointFields ) )
|
, Representable Double ( ℝ ( Length pointFields ) )
|
||||||
, DiffInterp 2 () ( ℝ ( Length pointFields ) )
|
, RepDim ( ℝ ( Length pointFields ) ) ~ Length pointFields
|
||||||
, DiffInterp 3 𝕀 ( ℝ ( Length pointFields ) )
|
, DiffInterp 2 ℝ ( Length pointFields )
|
||||||
|
, DiffInterp 3 𝕀 ( Length pointFields )
|
||||||
)
|
)
|
||||||
=> PointFields pointFields where { }
|
=> PointFields pointFields where { }
|
||||||
instance ( KnownSymbols pointFields, Typeable pointFields
|
instance ( KnownSymbols pointFields, Typeable pointFields
|
||||||
, Serialisable ( Record pointFields )
|
, Serialisable ( Record pointFields )
|
||||||
, Show ( Record pointFields )
|
, Show ( Record pointFields )
|
||||||
|
, Show ( ℝ ( Length pointFields ) )
|
||||||
, NFData ( Record pointFields )
|
, NFData ( Record pointFields )
|
||||||
, Representable Double ( ℝ ( Length pointFields ) )
|
, Representable Double ( ℝ ( Length pointFields ) )
|
||||||
, DiffInterp 2 () ( ℝ ( Length pointFields ) )
|
, RepDim ( ℝ ( Length pointFields ) ) ~ Length pointFields
|
||||||
, DiffInterp 3 𝕀 ( ℝ ( Length pointFields ) )
|
, DiffInterp 2 ℝ ( Length pointFields )
|
||||||
|
, DiffInterp 3 𝕀 ( Length pointFields )
|
||||||
)
|
)
|
||||||
=> PointFields pointFields where { }
|
=> PointFields pointFields where { }
|
||||||
|
|
||||||
|
|
|
@ -48,7 +48,6 @@ import qualified Data.Text as Text
|
||||||
( pack, unpack )
|
( pack, unpack )
|
||||||
|
|
||||||
-- MetaBrush
|
-- MetaBrush
|
||||||
import Math.Algebra.Dual
|
|
||||||
import Math.Differentiable
|
import Math.Differentiable
|
||||||
import Math.Interval
|
import Math.Interval
|
||||||
import Math.Linear
|
import Math.Linear
|
||||||
|
@ -99,19 +98,6 @@ deriving via ( T ( ℝ ( Length ks ) ) )
|
||||||
instance Module Double ( T ( ℝ ( Length ks ) ) )
|
instance Module Double ( T ( ℝ ( Length ks ) ) )
|
||||||
=> Module Double ( T ( Record ks ) )
|
=> Module Double ( T ( Record ks ) )
|
||||||
|
|
||||||
deriving via ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
instance Semigroup ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
=> Semigroup ( T ( 𝕀 ( Record ks ) ) )
|
|
||||||
deriving via ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
instance Monoid ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
=> Monoid ( T ( 𝕀 ( Record ks ) ) )
|
|
||||||
deriving via ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
instance Group ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
=> Group ( T ( 𝕀 ( Record ks ) ) )
|
|
||||||
deriving via ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
instance Module ( 𝕀 Double ) ( T ( 𝕀ℝ ( Length ks ) ) )
|
|
||||||
=> Module ( 𝕀 Double ) ( T ( 𝕀 ( Record ks ) ) )
|
|
||||||
|
|
||||||
instance ( Act ( T ( ℝ ( Length ks ) ) ) ( ℝ ( Length ks ) )
|
instance ( Act ( T ( ℝ ( Length ks ) ) ) ( ℝ ( Length ks ) )
|
||||||
, Semigroup ( T ( ℝ ( Length ks ) ) ) )
|
, Semigroup ( T ( ℝ ( Length ks ) ) ) )
|
||||||
=> Act ( T ( Record ks ) ) ( Record ks ) where
|
=> Act ( T ( Record ks ) ) ( Record ks ) where
|
||||||
|
@ -121,39 +107,11 @@ instance ( Torsor ( T ( ℝ ( Length ks ) ) ) ( ℝ ( Length ks ) )
|
||||||
=> Torsor ( T ( Record ks ) ) ( Record ks ) where
|
=> Torsor ( T ( Record ks ) ) ( Record ks ) where
|
||||||
MkR g --> MkR a = T $ MkR $ unT $ g --> a
|
MkR g --> MkR a = T $ MkR $ unT $ g --> a
|
||||||
|
|
||||||
instance ( Act ( T ( 𝕀ℝ ( Length ks ) ) ) ( 𝕀ℝ ( Length ks ) )
|
|
||||||
, Semigroup ( T ( 𝕀ℝ ( Length ks ) ) ) )
|
|
||||||
=> Act ( T ( 𝕀 ( Record ks ) ) ) ( 𝕀 ( Record ks ) ) where
|
|
||||||
T ( 𝕀 ( MkR g_lo ) ( MkR g_hi ) )
|
|
||||||
• 𝕀 ( MkR a_lo ) ( MkR a_hi )
|
|
||||||
= case T ( 𝕀 g_lo g_hi ) • 𝕀 a_lo a_hi of
|
|
||||||
𝕀 b_lo b_hi ->
|
|
||||||
𝕀 ( MkR b_lo ) ( MkR b_hi )
|
|
||||||
instance ( Torsor ( T ( 𝕀ℝ ( Length ks ) ) ) ( 𝕀ℝ ( Length ks ) )
|
|
||||||
, Group ( T ( 𝕀ℝ ( Length ks ) ) ) )
|
|
||||||
=> Torsor ( T ( 𝕀 ( Record ks ) ) ) ( 𝕀 ( Record ks ) ) where
|
|
||||||
𝕀 ( MkR a_lo ) ( MkR a_hi )
|
|
||||||
--> 𝕀 ( MkR b_lo ) ( MkR b_hi )
|
|
||||||
= case 𝕀 a_lo a_hi --> 𝕀 b_lo b_hi of
|
|
||||||
T ( 𝕀 c_lo c_hi ) ->
|
|
||||||
T ( 𝕀 ( MkR c_lo ) ( MkR c_hi ) )
|
|
||||||
|
|
||||||
type instance RepDim ( Record ks ) = Length ks
|
type instance RepDim ( Record ks ) = Length ks
|
||||||
deriving newtype instance ( KnownNat (Length ks)
|
deriving newtype instance ( KnownNat (Length ks)
|
||||||
, Representable r ( ℝ ( Length ks ) ) )
|
, Representable r ( ℝ ( Length ks ) ) )
|
||||||
=> Representable r ( Record ks )
|
=> Representable r ( Record ks )
|
||||||
|
|
||||||
type instance D k ( Record ks ) = D k ( ℝ ( Length ks ) )
|
|
||||||
deriving newtype instance HasChainRule Double 2 ( ℝ ( Length ks ) )
|
|
||||||
=> HasChainRule Double 2 ( Record ks )
|
|
||||||
|
|
||||||
deriving via 𝕀ℝ ( Length ks )
|
|
||||||
instance HasChainRule ( 𝕀 Double ) 2 ( 𝕀ℝ ( Length ks ) )
|
|
||||||
=> HasChainRule ( 𝕀 Double ) 2 ( 𝕀 ( Record ks ) )
|
|
||||||
deriving via 𝕀ℝ ( Length ks )
|
|
||||||
instance HasChainRule ( 𝕀 Double ) 3 ( 𝕀ℝ ( Length ks ) )
|
|
||||||
=> HasChainRule ( 𝕀 Double ) 3 ( 𝕀 ( Record ks ) )
|
|
||||||
|
|
||||||
--------------------------------------------------------------------------------
|
--------------------------------------------------------------------------------
|
||||||
|
|
||||||
type Length :: [ k ] -> Nat
|
type Length :: [ k ] -> Nat
|
||||||
|
@ -180,8 +138,10 @@ intersect :: forall r1 r2 l1 l2
|
||||||
, l1 ~ Length r1, l2 ~ Length r2
|
, l1 ~ Length r1, l2 ~ Length r2
|
||||||
, Representable Double ( ℝ l1 )
|
, Representable Double ( ℝ l1 )
|
||||||
, Representable Double ( ℝ l2 )
|
, Representable Double ( ℝ l2 )
|
||||||
, Differentiable 2 () ( ℝ l2 )
|
, Show ( ℝ l1 )
|
||||||
, Differentiable 3 𝕀 ( ℝ l2 )
|
, Show ( ℝ l2 )
|
||||||
|
, Differentiable 2 ℝ l2
|
||||||
|
, Differentiable 3 𝕀 l2
|
||||||
)
|
)
|
||||||
=> Intersection r1 r2
|
=> Intersection r1 r2
|
||||||
intersect
|
intersect
|
||||||
|
@ -211,8 +171,9 @@ data Intersection r1 r2 where
|
||||||
. ( l12 ~ Length r1r2
|
. ( l12 ~ Length r1r2
|
||||||
, KnownSymbols r1r2
|
, KnownSymbols r1r2
|
||||||
, Representable Double ( ℝ l12 )
|
, Representable Double ( ℝ l12 )
|
||||||
, Differentiable 2 () ( ℝ l12 )
|
, Show ( ℝ l12 )
|
||||||
, Differentiable 3 𝕀 ( ℝ l12 )
|
, Differentiable 2 ℝ l12
|
||||||
|
, Differentiable 3 𝕀 l12
|
||||||
)
|
)
|
||||||
=> { project1 :: Record r1 -> Record r1r2
|
=> { project1 :: Record r1 -> Record r1r2
|
||||||
-- ^ project out fields present in both rows
|
-- ^ project out fields present in both rows
|
||||||
|
@ -237,9 +198,10 @@ doIntersection
|
||||||
=> ( forall r1r2 l12.
|
=> ( forall r1r2 l12.
|
||||||
( r1r2 ~ Intersect r1 r2
|
( r1r2 ~ Intersect r1 r2
|
||||||
, KnownSymbols r1r2, l12 ~ Length r1r2
|
, KnownSymbols r1r2, l12 ~ Length r1r2
|
||||||
, Differentiable 2 () ( ℝ l12 )
|
, Differentiable 2 ℝ l12
|
||||||
, Differentiable 3 𝕀 ( ℝ l12 )
|
, Differentiable 3 𝕀 l12
|
||||||
, Representable Double ( ℝ l12 )
|
, Representable Double ( ℝ l12 )
|
||||||
|
, Show ( ℝ l12 )
|
||||||
)
|
)
|
||||||
=> Proxy# r1r2 -> Vec l12 ( Fin l1 ) -> Vec l12 ( Fin l2 ) -> kont )
|
=> Proxy# r1r2 -> Vec l12 ( Fin l1 ) -> Vec l12 ( Fin l2 ) -> kont )
|
||||||
-> kont
|
-> kont
|
||||||
|
|
Loading…
Reference in a new issue