Permalink
Browse files

Merge pull request #381 from SkySkimmer/fixes

Fixes
  • Loading branch information...
2 parents 1ed6fbc + aab8418 commit 31ec061128368242df3694f9f0391ed72d54b731 @andrejbauer andrejbauer committed Mar 8, 2017
Showing with 7 additions and 5 deletions.
  1. +3 −1 Makefile
  2. +4 −4 examples/bool.m31
View
@@ -93,9 +93,11 @@ uninstall-emacs:
rm -f $(SHARE_DIR)/emacs/site-lisp/andromeda.el $(SHARE_DIR)/emacs/site-lisp/andromeda-autoloads.el
install-lib:
- install -d $(LIB_DIR)
+ install -d $(LIB_DIR)/std
install -m 644 prelude.m31 $(LIB_DIR)/prelude.m31
+ cp -r std/* $(LIB_DIR)/std/
uninstall-lib:
+ rm -rf $(LIB_DIR)/std/*
rm -f $(LIB_DIR)/prelude.m31
rmdir $(LIB_DIR) || true
View
@@ -44,12 +44,12 @@ let bool_disjoint : true ≡ false → empty =
now betas = add_betas [ind_bool_true] in
p : unit == empty in
now betas = add_betas [p] in
- let u = {} in u : empty
+ let u = tt in u : empty
(* let's be less careful. *)
-now betas = add_beta ind_bool_true betas
-now betas = add_beta ind_bool_false betas
+now betas = add_beta ind_bool_true
+now betas = add_beta ind_bool_false
let bool_disjoint' : true == false → empty = λ p,
let P = λ (b : bool), ind_bool (λ (_ : bool), Type) unit empty b in
@@ -62,7 +62,7 @@ let bool_disjoint' : true == false → empty = λ p,
let p = p : unit == empty in
now betas = add_betas [p] in
- let u = {} in u : empty
+ let u = tt in u : empty
(* {} : empty *)
do bool_disjoint'

0 comments on commit 31ec061

Please sign in to comment.