egison-5.0.0: lib/math/geometry/differential-form.egi

def dfNormalize {Num a} (X: DiffForm a) : DiffForm a :=
  let p := dfOrder X
      (es, os) := evenAndOddPermutations p
   in withSymbols [i]
        (sum (map (\σ -> subrefs X (map 1#i_(σ $1) (between 1 p))) es)
       - sum (map (\σ -> subrefs X (map 1#i_(σ $1) (between 1 p))) os))
       / fact p

def antisymmetrize {Num a} : DiffForm a -> DiffForm a := dfNormalize

def wedge {Num a} (X: DiffForm a) (Y: DiffForm a) : DiffForm a := X !. Y

infixl expression 7 ∧

def (∧) {Num a} : DiffForm a -> DiffForm a -> DiffForm a := wedge

def Lie.wedge {Num a} (X: DiffForm a) (Y: DiffForm a) : DiffForm a := 
  X !. Y - Y !. X

def ι {Num a} (X: DiffForm a) (Y: DiffForm a) : DiffForm a := 
  withSymbols [i] dfOrder Y * (X...~i . dfNormalize Y..._i)

--def Lie {Num a} (X: DiffForm a) (Y: DiffForm a) : DiffForm a :=
--  match dfOrder Y as integer with
--    | #0 -> ι X (d Y)
--    | #N -> d (ι X Y)
--    | _ -> ι X (d Y) + d (ι X Y)

-- sortWithSign is now implemented as a primitive function in Haskell
-- See hs-src/Language/Egison/Primitives.hs