Commit 6c465ecb authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Don't use norm, it produces huge output

parent 8e86815d
......@@ -70,8 +70,6 @@ let myCell : PromCell ::= [ get = ς(self : PrivateCell) self.contents;
set = ς(self : PrivateCell) λ(n : Nat) self.contents := n;
contents = ς(self : PrivateCell) 0 ].
norm myCell.
print "\nSubtyping: Checking (myCell.set 42).get = 42 : Nat.\n".
check (myCell.set 42).get = 42 : Nat.
......
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