add DimEqs.zeroEq
This commit is contained in:
parent
d52d1c3181
commit
8006ae4c40
1 changed files with 4 additions and 0 deletions
|
@ -25,6 +25,10 @@ data DimEq : Nat -> Type where
|
|||
%name DimEq eqs
|
||||
|
||||
|
||||
export
|
||||
zeroEq : DimEq 0
|
||||
zeroEq = C [<]
|
||||
|
||||
export
|
||||
new' : (d : Nat) -> DimEq' d
|
||||
new' 0 = [<]
|
||||
|
|
Loading…
Reference in a new issue