We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 0b71a99 commit 944bc3cCopy full SHA for 944bc3c
src/Tactics.lidr
@@ -366,20 +366,6 @@ derived at once.
366
Note that we need to pass the parameter \idr{eqinj} which will be bound to
367
equations that \idr{injective} generates.
368
369
-
370
-==== Exercise: 1 star (inversion_ex3)
371
372
-> inversion_ex3 : (x, y, z : a) -> (l, j : List a) ->
373
-> x :: y :: l = z :: j ->
374
-> y :: l = x :: j ->
375
-> x = y
376
-> inversion_ex3 = ?remove_me3 -- %runElab inversion_ex3_tac
377
-> where
378
-> inversion_ex3_tac : Elab ()
379
-> inversion_ex3_tac = ?inversion_ex3_tac_rhs
380
381
-$\square$
382
383
\todo[inline]{Remove when a release with
384
https://github.com/idris-lang/Idris-dev/pull/3925 happens}
385
0 commit comments