mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-30 07:02:24 +03:00
18 lines
281 B
Idris
18 lines
281 B
Idris
|
module Issue833
|
||
|
|
|
||
|
|
import Data.Fin
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
data Singleton : Nat -> Type where
|
||
|
|
Sing : {n : Nat} -> Singleton n
|
||
|
|
|
||
|
|
f : (n : Singleton Z) -> n === Sing
|
||
|
|
f = \ Sing => Refl
|
||
|
|
|
||
|
|
g : (k : Fin 1) -> k === FZ
|
||
|
|
g = \ FZ => Refl
|
||
|
|
|
||
|
|
sym : {t, u : a} -> t === u -> u === t
|
||
|
|
sym = \Refl => Refl
|