trepplein

Lean type-checker written in Scala. (by gebner)

Trepplein Alternatives

Similar projects and alternatives to trepplein

  • holbert

    A graphical interactive proof assistant designed for education

  • CoqGym

    A Learning Environment for Theorem Proving with the Coq proof assistant

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • hott3

    HoTT in Lean 3

  • scala

    45 trepplein VS scala

    Scala 2 compiler and standard library. Bugs at https://github.com/scala/bug; Scala 3 at https://github.com/scala/scala3

  • Play

    31 trepplein VS Play

    The Community Maintained High Velocity Web Framework For Java and Scala.

  • nanoda_lib

    Library implementing type inference/checking functionality based on the Lean theorem prover

  • Lila

    591 trepplein VS Lila

    Discontinued ♞ lichess.org: the forever free, adless and open source chess server ♞ [Moved to: https://github.com/lichess-org/lila] (by ornicar)

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a better trepplein alternative or higher similarity.

trepplein reviews and mentions

Posts with mentions or reviews of trepplein. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-03-04.
  • Automated Theorem Provers?
    2 projects | /r/math | 4 Mar 2021
    The default kernel used is fairly large, since it does some optimisations for interactivity. However there are 3 independent checkers for Lean's output format, https://github.com/gebner/trepplein, https://github.com/leanprover/lean/tree/master/src/checker and https://github.com/leanprover/tc . They're all fairly small, with leanchecker being less than 1000 loc.
  • Formalising Mathematics: An Introduction
    2 projects | news.ycombinator.com | 21 Feb 2021
    Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean, e.g. [1].

    Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics, making it way more powerful than metamath.

    [1] https://github.com/gebner/trepplein/tree/master/src/main/sca...

Stats

Basic trepplein repo stats
2
26
0.0
about 2 years ago

gebner/trepplein is an open source project licensed under Apache License 2.0 which is an OSI approved license.

The primary programming language of trepplein is Scala.


Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com