{"action":"created","comment":{"url":"https://api.github.com/repos/gapt/gapt/pulls/comments/168097467","pull_request_review_id":96406304,"id":168097467,"diff_hunk":"@@ -0,0 +1,316 @@\n+package at.logic.gapt.proofs.nd\n+\n+import at.logic.gapt.expr.{ App, typeVariables, Ty, _ }\n+import at.logic.gapt.proofs.Context.{ BaseTypes, InductiveType, PrimRecFun, StructurallyInductiveTypes }\n+import at.logic.gapt.proofs._\n+import at.logic.gapt.proofs.nd._\n+import at.logic.gapt.utils.NameGenerator\n+\n+object MRealizability {\n+\n+  implicit var systemT: Context = Context.empty\n+\n+  def setSystemT( ctx: Context ): Unit = {\n+\n+    systemT = ctx\n+\n+    // add recursors for all inductive types\n+    for ( ( name, constructors ) <- systemT.get[StructurallyInductiveTypes].constructors.filter( _._1 != \"o\" ) ) {\n+      val typ = systemT.get[BaseTypes].baseTypes( name )\n+      val argTypes = constructors.map( x => x -> FunctionType.unapply( x.ty ).get._2 ) toMap\n+      val resultVariable = TVar( new NameGenerator( typeVariables( typ ) map ( _.name ) ).fresh( \"a\" ) )\n+      val ngTermVariableNames = new NameGenerator( systemT.constants map ( _.name ) )\n+\n+      val constrVars = constructors.map( x => x -> Var(\n+        ngTermVariableNames.fresh( \"x\" ),\n+        argTypes( x ).foldRight( resultVariable: Ty )( ( y, z ) => if ( y == typ ) typ ->: resultVariable ->: z else y ->: z ) ) ) toMap\n+\n+      val recursortype = constructors.foldRight( typ ->: resultVariable: Ty )( ( x, y ) => constrVars( x ).ty ->: y )\n+      val recursor = Const( name + \"Rec\", recursortype, typeVariables( recursortype ).toList )\n+      val argVars = argTypes.map( x => x._1 -> x._2.map( y => Var( ngTermVariableNames.fresh( \"x\" ), y ) ) )\n+\n+      val equations = constructors.map( x =>\n+        (\n+          App( recursor, constrVars.values.toVector :+ App( x, argVars( x ) ) ),\n+          argVars( x ).foldLeft( constrVars( x ): Expr )( ( y, z ) => if ( z.ty == typ ) App( App( y, z ), App( recursor, constrVars.values.toVector :+ z ) ) else App( y, z ) ) ) )\n+\n+      systemT += PrimRecFun( List( ( recursor, equations ) ) )\n+    }\n+\n+    // add conjuctive type, pairs, projections and their reduction rules\n+    val a = TVar( \"a\" )\n+    val b = TVar( \"b\" )\n+    val conj = TBase( \"conj\", a, b )\n+    val pair = Const( \"pair\", a ->: b ->: conj, List( a, b ) )\n+    systemT += InductiveType( conj, pair )\n+    val pi1 = Const( \"pi1\", conj ->: a, List( a, b ) )\n+    val pi2 = Const( \"pi2\", conj ->: b, List( a, b ) )\n+    val x: Expr = Var( \"x\", a )\n+    val y: Expr = Var( \"y\", b )\n+    systemT += PrimRecFun( List(\n+      ( pi1, List(\n+        ( App( pi1, App( pair, List( x, y ) ) ), x ) ) ) ) )( systemT )\n+    systemT += PrimRecFun( List(\n+      ( pi2, List(\n+        ( App( pi2, App( pair, List( x, y ) ) ), y ) ) ) ) )( systemT )\n+\n+    // add a term+type to represent the empty program\n+    systemT += InductiveType(\n+      ty\"1\",\n+      hoc\"i : 1\" )\n+  }\n+\n+  def mrealize( proof: NDProof )( implicit ctx: Context ): Expr = {\n+\n+    setSystemT( ctx )\n+\n+    mrealizeCases( proof )\n+\n+  }\n+\n+  def mrealizeCases( proof: NDProof ): Expr = {\n+\n+    normalize( proof match {\n+      case WeakeningRule( subProof, formula ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ) )\n+\n+      case ContractionRule( subProof, aux1, aux2 ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ) )\n+\n+      case LogicalAxiom( formula ) =>\n+        Abs( freeVariables( proof.conclusion ).toSeq :+ Var( \"x\", flat( formula ) ), Var( \"x\", flat( formula ) ) )\n+\n+      case AndElim1Rule( subProof ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pi1(${App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )})\" )\n+\n+      case AndElim2Rule( subProof ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pi2(${App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )})\" )\n+\n+      case AndIntroRule( leftSubproof, rightSubproof ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pair(${\n+            App( mrealizeCases( leftSubproof ), freeVariables( leftSubproof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )\n+          },${\n+            App( mrealizeCases( rightSubproof ), freeVariables( rightSubproof.conclusion ).toSeq ++ variablesAntPremise( proof, 1 ) )\n+          })\" )\n+\n+      case OrElimRule( leftSubProof, middleSubProof, aux1, rightSubProof, aux2 ) =>\n+        val realizerAOrB = App( mrealizeCases( leftSubProof ), freeVariables( leftSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"natRec(${\n+            App( mrealizeCases( middleSubProof ), freeVariables( middleSubProof.conclusion ).toSeq ++ insertIndex( variablesAntPremise( proof, 1 ), aux1,\n+              App( le\"pi1(pi2($realizerAOrB))\", le\"i\" ) ) )\n+          },${\n+            Abs( Var( \"z\", ty\"nat\" ), Abs(\n+              Var( \"z\", flat( proof.conclusion.succedent( 0 ) ) ),\n+              App( mrealizeCases( rightSubProof ), freeVariables( rightSubProof.conclusion ).toSeq ++ insertIndex( variablesAntPremise( proof, 2 ), aux2,\n+                App( le\"pi2(pi2($realizerAOrB))\", Abs( Var( \"z\", ty\"1\" ), le\"i\" ) ) ) ) ) )\n+          },pi1($realizerAOrB))\" )\n+\n+      case OrIntro1Rule( subProof, rightDisjunct ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pair(0,pair(${\n+            Abs( Var( \"z\", ty\"1\" ), App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ) )\n+          }, ${\n+            Abs( Var( \"z\", ty\"1>1\" ), Var( \"z\", flat( rightDisjunct ) ) )\n+          }))\" )\n+\n+      case OrIntro2Rule( subProof, leftDisjunct ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pair(s(0),pair(${\n+            Abs( Var( \"z\", ty\"1\" ), Var( \"z\", flat( leftDisjunct ) ) )\n+          }, ${\n+            Abs( Var( \"z\", ty\"1 > 1\" ), App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ) )\n+          }))\" )\n+\n+      case ImpElimRule( leftSubProof, rightSubProof ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App(\n+            App( mrealizeCases( leftSubProof ), freeVariables( leftSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ),\n+            App( mrealizeCases( rightSubProof ), freeVariables( rightSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 1 ) ) ) )\n+\n+      case ImpIntroRule( subProof, aux ) =>\n+        val extraVar = Var( \"z\", flat( subProof.conclusion( aux ) ) )\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          Abs(\n+            extraVar,\n+            App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ insertIndex( variablesAntPremise( proof, 0 ), aux, extraVar ) ) ) )\n+\n+      case NegElimRule( leftSubProof, rightSubProof ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App(\n+            App( mrealizeCases( leftSubProof ), freeVariables( leftSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ),\n+            App( mrealizeCases( rightSubProof ), freeVariables( rightSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 1 ) ) ) )\n+\n+      case NegIntroRule( subProof, aux ) =>\n+        val extraVar = Var( \"z\", flat( subProof.conclusion( aux ) ) )\n+        Abs( freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ), Abs(\n+          extraVar,\n+          App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ insertIndex( variablesAntPremise( proof, 0 ), aux, extraVar ) ) ) )\n+\n+      case TopIntroRule() =>\n+        val varr = Var( \"z\", ty\"1\" )\n+        Abs( varr, varr )\n+\n+      case BottomElimRule( subProof, mainFormula ) =>\n+        Abs( freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ), Var( \"z\", flat( mainFormula ) ) )\n+\n+      case ForallIntroRule( subProof, eigenVariable, quantifiedVariable ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ) :+ eigenVariable,\n+          App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) ) )\n+\n+      case ForallElimRule( subProof, term ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) :+ term ) )\n+\n+      case ExistsIntroRule( subProof, formula, term, variable ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          le\"pair($term,${App( mrealizeCases( subProof ), freeVariables( subProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )})\" )\n+\n+      case ExistsElimRule( leftSubProof, rightSubProof, aux, eigenVariable ) =>\n+        Abs( freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ), App(\n+          mrealizeCases( rightSubProof ),\n+          freeVariables( rightSubProof.conclusion ).toSeq.map {\n+            case `eigenVariable` =>\n+              le\"pi1(${App( mrealizeCases( leftSubProof ), freeVariables( leftSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )})\"\n+            case x => x\n+          } ++ insertIndex( variablesAntPremise( proof, 1 ), aux,\n+            le\"pi2(${App( mrealizeCases( leftSubProof ), freeVariables( leftSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )})\" ) ) )\n+\n+      // only to be used when mainFormula is an equation\n+      case TheoryAxiom( mainFormula ) =>\n+        Abs( freeVariables( mainFormula ).toSeq, le\"i : 1\" )\n+\n+      case EqualityElimRule( leftSubProof, rightSubProof, formulaA, variablex ) =>\n+        Abs(\n+          freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ),\n+          App( mrealizeCases( rightSubProof ), freeVariables( rightSubProof.conclusion ).toSeq ++ variablesAntPremise( proof, 1 ) ) )\n+\n+      case EqualityIntroRule( term ) =>\n+        Abs( freeVariables( proof.conclusion ).toSeq, le\"i\" )\n+\n+      // Works only for the type of natural numbers at the moment\n+      // Assumes that the induction cases for the constructors are in the same order as the inductive type definition in the context.\n+      case InductionRule( cases, formula, term ) =>\n+        val extraVar = Var( \"z\", flat( proof.conclusion( Suc( 0 ) ) ) )\n+        val mrealizerBaseCase = App( mrealizeCases( cases( 0 ).proof ), freeVariables( cases( 0 ).proof.conclusion ).toSeq ++ variablesAntPremise( proof, 0 ) )\n+        val mrealizerInductionCase = Abs( cases( 1 ).eigenVars :+ extraVar, App(\n+          mrealizeCases( cases( 1 ).proof ),\n+          freeVariables( cases( 1 ).proof.conclusion ).toSeq ++ insertIndex( variablesAntPremise( proof, 1 ), cases( 1 ).hypotheses( 0 ), extraVar ) ) )\n+        Abs( freeVariables( proof.conclusion ).toSeq ++ variablesAntConclusion( proof ), le\"natRec($mrealizerBaseCase,$mrealizerInductionCase,$term)\" )\n+\n+      case ExcludedMiddleRule( leftSubProof, aux1, rightSubProof, aux2 ) =>\n+        throw new MRealizerCreationException( proof.longName, \"This rule is not admitted in Heyting Arithmetic.\" )\n+    } )\n+  }\n+\n+  def flat( formula: Formula ): Ty = formula match {\n+    case Bottom()                         => ty\"1\"\n+    case Top()                            => flat( Imp( Bottom(), Bottom() ) )\n+    case Eq( _, _ )                       => ty\"1\"\n+    case Atom( _, _ )                     => ty\"1\" // ?","path":"core/src/main/scala/at/logic/gapt/proofs/nd/m-realizability.scala","position":229,"original_position":229,"commit_id":"f75fb2b14e5390a448a1c12b84c29039a8b74bcb","original_commit_id":"f75fb2b14e5390a448a1c12b84c29039a8b74bcb","user":{"login":"gebner","id":313929,"avatar_url":"https://avatars1.githubusercontent.com/u/313929?v=4","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"body":"This `?` is actually an interesting consideration: we might want to interpret certain atoms as non-unit types.\r\n\r\nFor example, consider the divisibility predicate `dvd` where `dvd x y` means that `x` divides `y`.  Think of `dvd x y` being defined as `∃z y = x*z`.  The natural interpretation for `dvd x y` would then be the `nat` type (the same as the definition), and not unit.","created_at":"2018-02-14T07:52:44Z","updated_at":"2018-02-14T07:54:16Z","html_url":"https://github.com/gapt/gapt/pull/685#discussion_r168097467","pull_request_url":"https://api.github.com/repos/gapt/gapt/pulls/685","author_association":"OWNER","_links":{"self":{"href":"https://api.github.com/repos/gapt/gapt/pulls/comments/168097467"},"html":{"href":"https://github.com/gapt/gapt/pull/685#discussion_r168097467"},"pull_request":{"href":"https://api.github.com/repos/gapt/gapt/pulls/685"}}},"pull_request":{"url":"https://api.github.com/repos/gapt/gapt/pulls/685","id":167914397,"html_url":"https://github.com/gapt/gapt/pull/685","diff_url":"https://github.com/gapt/gapt/pull/685.diff","patch_url":"https://github.com/gapt/gapt/pull/685.patch","issue_url":"https://api.github.com/repos/gapt/gapt/issues/685","number":685,"state":"open","locked":false,"title":"Modified realizability","user":{"login":"gebner","id":313929,"avatar_url":"https://avatars1.githubusercontent.com/u/313929?v=4","gravatar_id":"","url":"https://api.github.com/users/gebner","html_url":"https://github.com/gebner","followers_url":"https://api.github.com/users/gebner/followers","following_url":"https://api.github.com/users/gebner/following{/other_user}","gists_url":"https://api.github.com/users/gebner/gists{/gist_id}","starred_url":"https://api.github.com/users/gebner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gebner/subscriptions","organizations_url":"https://api.github.com/users/gebner/orgs","repos_url":"https://api.github.com/users/gebner/repos","events_url":"https://api.github.com/users/gebner/events{/privacy}","received_events_url":"https://api.github.com/users/gebner/received_events","type":"User","site_admin":false},"body":"(As usual, I'm just making a PR so that I can see all changes at a glance and add review comments.)","created_at":"2018-02-08T09:15:51Z","updated_at":"2018-02-14T07:54:16Z","closed_at":null,"merged_at":null,"merge_commit_sha":"fef3d5a71745290429ce12b3eeb74353104251c9","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/gapt/gapt/pulls/685/commits","review_comments_url":"https://api.github.com/repos/gapt/gapt/pulls/685/comments","review_comment_url":"https://api.github.com/repos/gapt/gapt/pulls/comments{/number}","comments_url":"https://api.github.com/repos/gapt/gapt/issues/685/comments","statuses_url":"https://api.github.com/repos/gapt/gapt/statuses/f75fb2b14e5390a448a1c12b84c29039a8b74bcb","head":{"label":"gapt:m-realizability","ref":"m-realizability","sha":"f75fb2b14e5390a448a1c12b84c29039a8b74bcb","user":{"login":"gapt","id":10725194,"avatar_url":"https://avatars0.githubusercontent.com/u/10725194?v=4","gravatar_id":"","url":"https://api.github.com/users/gapt","html_url":"https://github.com/gapt","followers_url":"https://api.github.com/users/gapt/followers","following_url":"https://api.github.com/users/gapt/following{/other_user}","gists_url":"https://api.github.com/users/gapt/gists{/gist_id}","starred_url":"https://api.github.com/users/gapt/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gapt/subscriptions","organizations_url":"https://api.github.com/users/gapt/orgs","repos_url":"https://api.github.com/users/gapt/repos","events_url":"https://api.github.com/users/gapt/events{/privacy}","received_events_url":"https://api.github.com/users/gapt/received_events","type":"Organization","site_admin":false},"repo":{"id":1971451,"name":"gapt","full_name":"gapt/gapt","owner":{"login":"gapt","id":10725194,"avatar_url":"https://avatars0.githubusercontent.com/u/10725194?v=4","gravatar_id":"","url":"https://api.github.com/users/gapt","html_url":"https://github.com/gapt","followers_url":"https://api.github.com/users/gapt/followers","following_url":"https://api.github.com/users/gapt/following{/other_user}","gists_url":"https://api.github.com/users/gapt/gists{/gist_id}","starred_url":"https://api.github.com/users/gapt/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gapt/subscriptions","organizations_url":"https://api.github.com/users/gapt/orgs","repos_url":"https://api.github.com/users/gapt/repos","events_url":"https://api.github.com/users/gapt/events{/privacy}","received_events_url":"https://api.github.com/users/gapt/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/gapt/gapt","description":"GAPT: General Architecture for Proof Theory","fork":false,"url":"https://api.github.com/repos/gapt/gapt","forks_url":"https://api.github.com/repos/gapt/gapt/forks","keys_url":"https://api.github.com/repos/gapt/gapt/keys{/key_id}","collaborators_url":"https://api.github.com/repos/gapt/gapt/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/gapt/gapt/teams","hooks_url":"https://api.github.com/repos/gapt/gapt/hooks","issue_events_url":"https://api.github.com/repos/gapt/gapt/issues/events{/number}","events_url":"https://api.github.com/repos/gapt/gapt/events","assignees_url":"https://api.github.com/repos/gapt/gapt/assignees{/user}","branches_url":"https://api.github.com/repos/gapt/gapt/branches{/branch}","tags_url":"https://api.github.com/repos/gapt/gapt/tags","blobs_url":"https://api.github.com/repos/gapt/gapt/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/gapt/gapt/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/gapt/gapt/git/refs{/sha}","trees_url":"https://api.github.com/repos/gapt/gapt/git/trees{/sha}","statuses_url":"https://api.github.com/repos/gapt/gapt/statuses/{sha}","languages_url":"https://api.github.com/repos/gapt/gapt/languages","stargazers_url":"https://api.github.com/repos/gapt/gapt/stargazers","contributors_url":"https://api.github.com/repos/gapt/gapt/contributors","subscribers_url":"https://api.github.com/repos/gapt/gapt/subscribers","subscription_url":"https://api.github.com/repos/gapt/gapt/subscription","commits_url":"https://api.github.com/repos/gapt/gapt/commits{/sha}","git_commits_url":"https://api.github.com/repos/gapt/gapt/git/commits{/sha}","comments_url":"https://api.github.com/repos/gapt/gapt/comments{/number}","issue_comment_url":"https://api.github.com/repos/gapt/gapt/issues/comments{/number}","contents_url":"https://api.github.com/repos/gapt/gapt/contents/{+path}","compare_url":"https://api.github.com/repos/gapt/gapt/compare/{base}...{head}","merges_url":"https://api.github.com/repos/gapt/gapt/merges","archive_url":"https://api.github.com/repos/gapt/gapt/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/gapt/gapt/downloads","issues_url":"https://api.github.com/repos/gapt/gapt/issues{/number}","pulls_url":"https://api.github.com/repos/gapt/gapt/pulls{/number}","milestones_url":"https://api.github.com/repos/gapt/gapt/milestones{/number}","notifications_url":"https://api.github.com/repos/gapt/gapt/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/gapt/gapt/labels{/name}","releases_url":"https://api.github.com/repos/gapt/gapt/releases{/id}","deployments_url":"https://api.github.com/repos/gapt/gapt/deployments","created_at":"2011-06-29T09:15:16Z","updated_at":"2018-02-05T07:37:38Z","pushed_at":"2018-02-13T22:46:06Z","git_url":"git://github.com/gapt/gapt.git","ssh_url":"git@github.com:gapt/gapt.git","clone_url":"https://github.com/gapt/gapt.git","svn_url":"https://github.com/gapt/gapt","homepage":"https://logic.at/gapt/","size":121814,"stargazers_count":38,"watchers_count":38,"language":"Scala","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":13,"mirror_url":null,"archived":false,"open_issues_count":48,"license":{"key":"gpl-3.0","name":"GNU General Public License v3.0","spdx_id":"GPL-3.0","url":"https://api.github.com/licenses/gpl-3.0"},"forks":13,"open_issues":48,"watchers":38,"default_branch":"master"}},"base":{"label":"gapt:master","ref":"master","sha":"b2dd4e65c0a23efc5e15e4b4088b10afd551b8ab","user":{"login":"gapt","id":10725194,"avatar_url":"https://avatars0.githubusercontent.com/u/10725194?v=4","gravatar_id":"","url":"https://api.github.com/users/gapt","html_url":"https://github.com/gapt","followers_url":"https://api.github.com/users/gapt/followers","following_url":"https://api.github.com/users/gapt/following{/other_user}","gists_url":"https://api.github.com/users/gapt/gists{/gist_id}","starred_url":"https://api.github.com/users/gapt/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gapt/subscriptions","organizations_url":"https://api.github.com/users/gapt/orgs","repos_url":"https://api.github.com/users/gapt/repos","events_url":"https://api.github.com/users/gapt/events{/privacy}","received_events_url":"https://api.github.com/users/gapt/received_events","type":"Organization","site_admin":false},"repo":{"id":1971451,"name":"gapt","full_name":"gapt/gapt","owner":{"login":"gapt","id":10725194,"avatar_url":"https://avatars0.githubusercontent.com/u/10725194?v=4","gravatar_id":"","url":"https://api.github.com/users/gapt","html_url":"https://github.com/gapt","followers_url":"https://api.github.com/users/gapt/followers","following_url":"https://api.github.com/users/gapt/following{/other_user}","gists_url":"https://api.github.com/users/gapt/gists{/gist_id}","starred_url":"https://api.github.com/users/gapt/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/gapt/subscriptions","organizations_url":"https://api.github.com/users/gapt/orgs","repos_url":"https://api.github.com/users/gapt/repos","events_url":"https://api.github.com/users/gapt/events{/privacy}","received_events_url":"https://api.github.com/users/gapt/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/gapt/gapt","description":"GAPT: General Architecture for Proof Theory","fork":false,"url":"https://api.github.com/repos/gapt/gapt","forks_url":"https://api.github.com/repos/gapt/gapt/forks","keys_url":"https://api.github.com/repos/gapt/gapt/keys{/key_id}","collaborators_url":"https://api.github.com/repos/gapt/gapt/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/gapt/gapt/teams","hooks_url":"https://api.github.com/repos/gapt/gapt/hooks","issue_events_url":"https://api.github.com/repos/gapt/gapt/issues/events{/number}","events_url":"https://api.github.com/repos/gapt/gapt/events","assignees_url":"https://api.github.com/repos/gapt/gapt/assignees{/user}","branches_url":"https://api.github.com/repos/gapt/gapt/branches{/branch}","tags_url":"https://api.github.com/repos/gapt/gapt/tags","blobs_url":"https://api.github.com/repos/gapt/gapt/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/gapt/gapt/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/gapt/gapt/git/refs{/sha}","trees_url":"https://api.github.com/repos/gapt/gapt/git/trees{/sha}","statuses_url":"https://api.github.com/repos/gapt/gapt/statuses/{sha}","languages_url":"https://api.github.com/repos/gapt/gapt/languages","stargazers_url":"https://api.github.com/repos/gapt/gapt/stargazers","contributors_url":"https://api.github.com/repos/gapt/gapt/contributors","subscribers_url":"https://api.github.com/repos/gapt/gapt/subscribers","subscription_url":"https://api.github.com/repos/gapt/gapt/subscription","commits_url":"https://api.github.com/repos/gapt/gapt/commits{/sha}","git_commits_url":"https://api.github.com/repos/gapt/gapt/git/commits{/sha}","comments_url":"https://api.github.com/repos/gapt/gapt/comments{/number}","issue_comment_url":"https://api.github.com/repos/gapt/gapt/issues/comments{/number}","contents_url":"https://api.github.com/repos/gapt/gapt/contents/{+path}","compare_url":"https://api.github.com/repos/gapt/gapt/compare/{base}...{head}","merges_url":"https://api.github.com/repos/gapt/gapt/merges","archive_url":"https://api.github.com/repos/gapt/gapt/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/gapt/gapt/downloads","issues_url":"https://api.github.com/repos/gapt/gapt/issues{/number}","pulls_url":"https://api.github.com/repos/gapt/gapt/pulls{/number}","milestones_url":"https://api.github.com/repos/gapt/gapt/milestones{/number}","notifications_url":"https://api.github.com/repos/gapt/gapt/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/gapt/gapt/labels{/name}","releases_url":"https://api.github.com/repos/gapt/gapt/releases{/id}","deployments_url":"https://api.github.com/repos/gapt/gapt/deployments","created_at":"2011-06-29T09:15:16Z","updated_at":"2018-02-05T07:37:38Z","pushed_at":"2018-02-13T22:46:06Z","git_url":"git://github.com/gapt/gapt.git","ssh_url":"git@github.com:gapt/gapt.git","clone_url":"https://github.com/gapt/gapt.git","svn_url":"https://github.com/gapt/gapt","homepage":"https://logic.at/gapt/","size":121814,"stargazers_count":38,"watchers_count":38,"language":"Scala","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":13,"mirror_url":null,"archived":false,"open_issues_count":48,"license":{"key":"gpl-3.0","name":"GNU General Public License v3.0","spdx_id":"GPL-3.0","url":"https://api.github.com/licenses/gpl-3.0"},"forks":13,"open_issues":48,"watchers":38,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/gapt/gapt/pulls/685"},"html":{"href":"https://github.com/gapt/gapt/pull/685"},"issue":{"href":"https://api.github.com/repos/gapt/gapt/issues/685"},"comments":{"href":"https://api.github.com/repos/gapt/gapt/issues/685/comments"},"review_comments":{"href":"https://api.github.com/repos/gapt/gapt/pulls/685/comments"},"review_comment":{"href":"https://api.github.com/repos/gapt/gapt/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/gapt/gapt/pulls/685/commits"},"statuses":{"href":"https://api.github.com/repos/gapt/gapt/statuses/f75fb2b14e5390a448a1c12b84c29039a8b74bcb"}},"author_association":"OWNER"}}
{"actor":{"display_login":"gebner"}}