annotate paper/src/env.agda @ 4:bf1f62556b81

add while_test_init_imple
author soto
date Thu, 11 Feb 2021 17:03:31 +0900
parents 959f4b34d6f4
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
3
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
1 record Envc : Set where
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
2 field
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
3 vari : ℕ
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
4 varn : ℕ
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
5 c10 : ℕ
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
6
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
7 makeEnv : ℕ → ℕ → ℕ → Envc
959f4b34d6f4 add final thesis
soto
parents:
diff changeset
8 makeEnv i n c = record { vari = i ; varn = n ; c10 = c }