Commit 7861eb68 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

New syntax for #NAME lines

parent edca5a50
#NAME dk_binary_nat
#NAME dk_binary_nat.
BNat : Type.
......
#NAME dk_bool
#NAME dk_bool.
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_char
#NAME dk_char.
(; 7bits (ascii) characters ;)
uT := pts.uT.
......
#NAME dk_domain
#NAME dk_domain.
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_logic
#NAME dk_logic.
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_machine_int
#NAME dk_machine_int.
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_nat
#NAME dk_nat.
Bool : Type := dk_bool.Bool.
......
#NAME dk_obj
#NAME dk_obj.
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_string
#NAME dk_string.
(; lists of ascii characters ;)
uT := pts.uT.
eT := pts.eT.
......
#NAME dk_type
#NAME dk_type.
Bool := dk_bool.Bool.
true := dk_bool.true.
......
#NAME pts
#NAME pts.
(; Encoding of the Pure Type System λΠ ;)
uT : Type.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment