File tree Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Expand file tree Collapse file tree 3 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -1161,7 +1161,7 @@ the value of \idr{b}.
1161
1161
\ todo[inline]{Remove when a release with
1162
1162
https : //github.com/idris-lang/Idris-dev/pull/3925 happens}
1163
1163
1164
- > Uninhabited (False = True ) where
1164
+ > implementation Uninhabited (False = True ) where
1165
1165
> uninhabited Refl impossible
1166
1166
1167
1167
> restricted_excluded_middle : (p <-> b = True) -> p `Either ` Not p
Original file line number Diff line number Diff line change @@ -88,7 +88,7 @@ about strings:
88
88
\ todo[inline]{Remove when a release with
89
89
https : //github.com/idris-lang/Idris-dev/pull/3925 happens}
90
90
91
- > Uninhabited (False = True ) where
91
+ > implementation Uninhabited (False = True ) where
92
92
> uninhabited Refl impossible
93
93
>
94
94
Original file line number Diff line number Diff line change @@ -379,7 +379,7 @@ $\square$
379
379
380
380
\ todo[inline]{Remove if https : //github.com/idris-lang/Idris-dev/pull/3925 is merged}
381
381
382
- > Uninhabited (False = True ) where
382
+ > implementation Uninhabited (False = True ) where
383
383
> uninhabited Refl impossible
384
384
385
385
\ todo[inline]{Edit }
You can’t perform that action at this time.
0 commit comments