
  0 | module Data.Materialise
  1 | 
  2 | ||| Used for `Data.Tensor` and structures thereof: directly evaluates the tensor
  3 | ||| instead of keeping it tabulated form
  4 | ||| There's probably a more principled solution
  5 | public export
  6 | interface Materialise a where
  7 |   constructor MkMaterialise
  8 |   materialise : a -> a
  9 |   ||| Extensionally the data is equivalent
 10 |   materialiseIsId : {x : a} -> materialise x = x
 11 | 
 12 | public export
 13 | Materialise Double where
 14 |   materialise = id
 15 |   materialiseIsId = Refl
 16 | 
 17 | public export
 18 | Materialise Integer where
 19 |   materialise = id
 20 |   materialiseIsId = Refl
 21 | 
 22 | public export
 23 | Materialise Nat where
 24 |   materialise = id
 25 |   materialiseIsId = Refl
 26 | 
 27 | public export
 28 | Materialise Unit where
 29 |   materialise = id
 30 |   materialiseIsId = Refl
 31 | 
 32 | public export
 33 | Materialise a => Materialise b => Materialise (a, b) where
 34 |   materialise (x, y) = (materialise x, materialise y)
 35 |   materialiseIsId {x=(a, b)} = cong2 (,) materialiseIsId materialiseIsId