Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Vendor Agda stdlib

  • Loading branch information...
commit fb8fd77f88475b9b85c3645d3ad9e65e608685ae 1 parent b72c796
Larry Diehl authored
View
22 LICENSE
@@ -0,0 +1,22 @@
+(The MIT License)
+
+Copyright (c) 2010 Larry Diehl
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+'Software'), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED 'AS IS', WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
View
43 README.md
@@ -1,39 +1,24 @@
-# Lemmachine
+Lemmachine
+==========
-## Setup
+## Setup ##
cabal install hack hack-handler-happstack
-## Running
+## Development ##
+
+We use a vendored modified Agda stdlib, so in Emacs:
+ M-x customize group
+ agda2
+
+Then add this to `Agda2 Include Dirs`:
+ ./vendor/stdlib/src
+
+## Running ##
Lemmachine statuses can presently be passed through to Hack.
To see this in action, run the following from the project root directory:
- agda -c -i . -i /path/to/agda-stdlib/src/ Lemmachine/Runner.agda
+ agda -c -i . -i ./vendor/stdlib/src Lemmachine/Runner.agda
./Runner
curl -i http://localhost:3000 && echo
-
-## License
-
-(The MIT License)
-
-Copyright (c) 2010 Larry Diehl
-
-Permission is hereby granted, free of charge, to any person obtaining
-a copy of this software and associated documentation files (the
-'Software'), to deal in the Software without restriction, including
-without limitation the rights to use, copy, modify, merge, publish,
-distribute, sublicense, and/or sell copies of the Software, and to
-permit persons to whom the Software is furnished to do so, subject to
-the following conditions:
-
-The above copyright notice and this permission notice shall be
-included in all copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED 'AS IS', WITHOUT WARRANTY OF ANY KIND,
-EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
-MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
-IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
-CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
-TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
-SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
View
3  vendor/stdlib/src/Relation/Binary/Core.agda
@@ -135,6 +135,9 @@ private
data _≡_ {a : Set} (x : a) : a → Set where
refl : x ≡ x
+ {-# BUILTIN EQUALITY _≡_ #-}
+ {-# BUILTIN REFL refl #-}
+
-- Nonequality.
_≢_ : {a : Set} a a Set
View
19 vendor/stdlib/src/Relation/Binary/PropositionalEquality/TrustMe.agda
@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- An equality postulate which evaluates
+------------------------------------------------------------------------
+
+module Relation.Binary.PropositionalEquality.TrustMe where
+
+open import Relation.Binary.PropositionalEquality
+
+private
+ primitive
+ primTrustMe : {A : Set}{a b : A} a ≡ b
+
+-- trustMe {a = x} {b = y} evaluates to refl if x and y are
+-- definitionally equal.
+--
+-- For an example of the use of trustMe, see Data.String._≟_.
+
+trustMe : {A : Set}{a b : A} a ≡ b
+trustMe = primTrustMe
Please sign in to comment.
Something went wrong with that request. Please try again.