blob: 0029760a72435f8d0d8ecfdaf948f6b44bad73f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
module Encoded.Fin
import public Data.Nat
import Data.Stream
import Encoded.Arith
import Encoded.Pair
import Term.Syntax
export
Fin : Nat -> Ty
Fin k = N
oldShow : Nat -> String
oldShow = show
export
zero : Term (Fin (S k)) ctx
zero = Zero
export
suc : Term (Fin k ~> Fin (S k)) ctx
suc = Abs' Suc
export
inject : Term (Fin k ~> Fin (S k)) ctx
inject = Id
export
absurd : {ty : Ty} -> Term (Fin 0 ~> ty) ctx
absurd = Arb
export
induct : {ty : Ty} -> Term (Fin (S k) ~> ty ~> (Fin k * ty ~> ty) ~> ty) ctx
induct = rec
export
forget : Term (Fin k ~> N) ctx
forget = Id
export
divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
divmod' k = Abs' (\n => App divmod [<n, Lit k])
|
