This file has been truncated, but you can view the full file.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
DEBUG:pijul::commands: get_wd: None | |
DEBUG:pijul::commands: path: "/home/lethom/Repos/lkn" | |
DEBUG:libpijul::record: children of current_inode 0000000000000000 | |
DEBUG:libpijul::record: iterating tree, starting from FileId { parent_inode: Inode(0000000000000000), basename: "" } | |
DEBUG:libpijul::record: calling record_all recursively, 397 | |
DEBUG:libpijul::record: realpath: "/home/lethom/Repos/lkn/LICENSE" | |
DEBUG:libpijul::record: inode: Inode(141c73e142d55979) | |
DEBUG:libpijul::record: header: Some(FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } }) | |
DEBUG:libpijul::record: current_node=FileHeader { metadata: FileMetadata(420), status: Ok, key: Key { patch: PatchId 0x85d31085e7e911f0, line: LineId(0x0200000000000000) } } | |
DEBUG:libpijul::record: old_attr=FileMetadata(420),int_attr=Some(FileMetadata(420)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* master | |
* feat(nestling): get the list of branches of a given repository | |
applied: | |
* master | |
deps: | |
* feat(nestling): get the name of a branch | |
applied: | |
* master | |
deps: | |
* feat(nestling): get the list of branches of a given repository |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE GADTs #-} | |
module Vec where | |
data Nat = Z | S Nat | |
data Vector a n where | |
VNil :: Vector a Z | |
(:-) :: a -> Vector a n -> Vector a (S n) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
λ pijul pull lthms@nest.pijul.com:pointfree/pijul --from-branch refactorings master pijul | |
Hash: AeHJpPsNz9ysK4b4otQVJfUMdBi0NeXSDndUwDNzDt3JSC8XjWTWxZbob1F-LWekLhszO10gt_8WwIB75NpMklY | |
Authors: ["pmeunier <pe@pijul.org>"] | |
Timestamp: 2017-09-01 07:01:18.120069075 UTC | |
New Cargo.lock | |
Shall I pull this patch? [ynkad] n | |
Hash: AQwJmpxgfJ6yB9U3DL1Tui8WZfLBUbI_RK8zGyu5105CiUvvWnNvv9Kxw-GPEEA9pwFO3D8xM8J4hrEkXZRej1Q | |
Authors: ["pmeunier <pe@pijul.org>"] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive sublist | |
{A: Type} | |
: list A -> list A -> Prop := | |
| elem_hit (a: A) | |
(l l': list A) | |
(H: sublist l l') | |
: sublist (cons a l) (cons a l') | |
| elem_next (a: A) | |
(l l': list A) | |
(H: sublist l l') |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE TypeOperators #-} | |
module Control.Monad.Chain.Fs | |
( -- * Functions | |
openFile | |
, closeFile | |
, getLine | |
, IO.IOMode(..) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/usr/bin/env stack | |
-- stack --resolver lts-10.4 script | |
import Test.Hspec | |
sup :: Int -> Int | |
sup x | |
| (x `mod` 10) /= 0 = x - (x `mod` 10) + 10 | |
| otherwise = 10 * sup (x `div` 10) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
│23:39:42 lthms | et je vais m’arrêter là pour ce soir | |
│23:39:49 | parce que dodo | |
│00:33:35 | je me suis relevé parce que j’arrivais pas à dormir à cause de ce truc |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Coq.Program.Program. | |
Require Import Coq.Arith.PeanoNat. | |
Require Import Recdef. | |
Require Import Omega. | |
Function sup | |
(n: nat) | |
{measure id} | |
: nat := | |
match n with |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Coq.Arith.Mult. | |
Inductive tree | |
(a: Type) | |
: Type := | |
| Leaf (x: a) | |
: tree a | |
| Node (x: a) | |
(l: tree a) | |
(r: tree a) |