Skip to content

Commit

Permalink
remove renamings (#3)
Browse files Browse the repository at this point in the history
  • Loading branch information
fblanqui authored Jun 24, 2024
1 parent f18d8e6 commit 05d3f31
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 10 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
*.lpo
10 changes: 0 additions & 10 deletions Main.lp
Original file line number Diff line number Diff line change
Expand Up @@ -25,13 +25,3 @@ symbol Rnotall a p : (Π t : τ a, π (¬ (p t)) → π ⊥) → π (¬ (∀ p))
symbol Rsubst a p (t1 t2 : τ a) : (π (¬ (t1 = t2)) → π ⊥) → (π (p t2) → π ⊥) → π (p t1) → π ⊥;
symbol Rconglr a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t1 = t2) → π ⊥;
symbol Rcongrl a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t2 = t1) → π ⊥;

// temporary renamings to be removed ultimately
symbol Type ≔ Set;
symbol ι : Set;
symbol τ ≔ τ;
symbol κ ≔ τ ι;
symbol ∀α [a] ≔ ∀ [a];
symbol ∃α [a] ≔ ∃ [a];
symbol =α [a] ≔ (=) [a];
symbol ϵ ≔ π;
1 change: 1 addition & 0 deletions lambdapi-zenon.opam
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ license: "CECILL-2.1"
homepage: "https://github.com/Deducteam/lambdapi-zenon"
bug-reports: "https://github.com/Deducteam/lambdapi-zenon/issues"
dev-repo: "git+https://github.com/Deducteam/lambdapi-zenon.git"
build: [ make ]
install: [ make "install" ]
depends: [
"lambdapi" {>= "2.3.0"}
Expand Down

0 comments on commit 05d3f31

Please sign in to comment.