fix sample

egison · Nov 25, 2022 · 4077410 · 4077410
1 parent 148866c
commit 4077410
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/sample/antisym.pegi b/sample/antisym.pegi
@@ -19,8 +19,4 @@
 (define (($antisym ($m : <Nat {} {}>) ($n : <Nat {} {}>) <Lte {} {m n}> <Lte {} {n m}>) : <Eq {<Nat {} {}> m} {n}>)
   {[[<zero> <zero> <lz #<zero>> <lz #<zero>>] <refl>]
    [[<suc $m'> <suc $n'> <ls #m' #n' $x> <ls #n' #m' $y>] (cong <Nat {} {}> <Nat {} {}> (λ [$k] <suc k>) m' n' (antisym m' n' x y))]})
-
-
-(define (($antisymx ($m : <Nat {} {}>) ($n : <Nat {} {}>) <Lte {} {m n}> <Lte {} {n m}>) : <Eq {<Nat {} {}> m} {n}>)
-  {[[<zero> <zero> <lz #<zero>> <lz #<zero>>] <refl>]})