{"header":{"message":"Add a basic CLI","description":null,"timestamp":"2021-11-02T14:18:40.712161121Z","authors":[{}]},"hash":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC","authors":[{"key":"HZVQFtjbhnRsZNcTqNkbgkDT47NMwiGoHjvCqCkuekqp"}],"deps":{"hashes":[["DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC","Add a basic CLI"],["AA",null]],"deps":[],"known":[]},"hunks":[{"FileAdd":{"meta":{"basename":"src","metadata":576},"path":"src","context":[{"change":1,"pos":0}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Pijul.lean","metadata":0},"path":"src/Pijul.lean","context":[{"change":0,"pos":15}],"contents":[{"Add":{"text":"import Pijul.Cli","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:68"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:69"}},{"Add":{"text":"def main (args : List String) : IO UInt32 := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:117"}},{"Add":{"text":" try","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:123"}},{"Add":{"text":" Pijul.cli args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:142"}},{"Add":{"text":" pure 0","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:153"}},{"Add":{"text":" catch e =>","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:166"}},{"Add":{"text":" IO.eprintln <| \"error: \" ++ toString e -- avoid \"uncaught exception: ...\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:244"}},{"Add":{"text":" pure 1","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:255"}}]}},{"FileAdd":{"meta":{"basename":"Pijul","metadata":576},"path":"src/Pijul","context":[{"change":0,"pos":15}],"contents":[]}},{"FileAdd":{"meta":{"basename":"Help.lean","metadata":0},"path":"src/Pijul/Help.lean","context":[{"change":0,"pos":274}],"contents":[{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:310"}},{"Add":{"text":"namespace Pijul","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:326"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:327"}},{"Add":{"text":"def usage := \"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:342"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:343"}},{"Add":{"text":"USAGE:","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:350"}},{"Add":{"text":" pijul [OPTIONS] ","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:378"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:379"}},{"Add":{"text":"OPTIONS:","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:388"}},{"Add":{"text":" --version print version and exit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:435"}},{"Add":{"text":" --help, -h print help of the program or a command and exit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:507"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:508"}},{"Add":{"text":"COMMANDS:\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:519"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:520"}},{"Add":{"text":"def helpCmd : (cmd : String) → String","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:560"}},{"Add":{"text":"| _ => usage","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:583"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:584"}},{"Add":{"text":"def help : (cmd? : Option String) → String","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:629"}},{"Add":{"text":"| some cmd => helpCmd cmd","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:655"}},{"Add":{"text":"| none => usage","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:671"}}]}},{"FileAdd":{"meta":{"basename":"Cli.lean","metadata":0},"path":"src/Pijul/Cli.lean","context":[{"change":0,"pos":274}],"contents":[{"Add":{"text":"import Pijul.Help","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:724"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:725"}},{"Add":{"text":"namespace Pijul ","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:742"}},{"Add":{"text":"open System","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:754"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:755"}},{"Add":{"text":"constant version: String := \"0.1.0\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:791"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:792"}},{"Add":{"text":"--------------------------------------------------------------------------------","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:873"}},{"Add":{"text":"-- # CLI Transformer Definition","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:905"}},{"Add":{"text":"--------------------------------------------------------------------------------","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:986"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:987"}},{"Add":{"text":"-- Involves trickery patterned after `MacroM`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1033"}},{"Add":{"text":"-- to allow `BuildMethods` to refer to `BuildM`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1081"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1082"}},{"Add":{"text":"constant CliMethodsRefPointed : PointedType.{0}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1130"}},{"Add":{"text":"def CliMethodsRef (m : Type → Type v) : Type := CliMethodsRefPointed.type","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1206"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1207"}},{"Add":{"text":"abbrev CliT (m : Type → Type v) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1244"}},{"Add":{"text":" ReaderT (CliMethodsRef m) <| StateT (List String) m","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1298"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1299"}},{"Add":{"text":"instance [Pure m] [Inhabited α] : Inhabited (CliT m α) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1359"}},{"Add":{"text":" ⟨fun _ _ => pure (Inhabited.default, Inhabited.default)⟩","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1422"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1423"}},{"Add":{"text":"structure CliMethods (m : Type → Type v) where","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1472"}},{"Add":{"text":" longOption : String → CliT m PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1511"}},{"Add":{"text":" longShortOption : String → CliT m PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1555"}},{"Add":{"text":" shortOption : Char → CliT m PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1593"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1594"}},{"Add":{"text":"instance [Pure m] : Inhabited (CliMethods m) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1642"}},{"Add":{"text":" ⟨Inhabited.default, Inhabited.default, Inhabited.default⟩","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1706"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1707"}},{"Add":{"text":"namespace CliMethodsRef","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1731"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1732"}},{"Add":{"text":"unsafe def mkImp (methods : CliMethods m) : CliMethodsRef m :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1795"}},{"Add":{"text":" unsafeCast methods","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1816"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1817"}},{"Add":{"text":"@[implementedBy mkImp]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1840"}},{"Add":{"text":"constant mk (methods : CliMethods m) : CliMethodsRef m :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1898"}},{"Add":{"text":" CliMethodsRefPointed.val","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1925"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1926"}},{"Add":{"text":"instance : Coe (CliMethods m) (CliMethodsRef m) := ⟨mk⟩","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:1986"}},{"Add":{"text":"instance [Pure m] : Inhabited (CliMethodsRef m) := ⟨mk Inhabited.default⟩","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2064"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2065"}},{"Add":{"text":"unsafe def getImp [Pure m] (self : CliMethodsRef m) : CliMethods m :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2135"}},{"Add":{"text":" unsafeCast self","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2153"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2154"}},{"Add":{"text":"@[implementedBy getImp]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2178"}},{"Add":{"text":"constant get [Pure m] (self : CliMethodsRef m) : CliMethods m","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2240"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2241"}},{"Add":{"text":"end CliMethodsRef","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2259"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2260"}},{"Add":{"text":"--------------------------------------------------------------------------------","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2341"}},{"Add":{"text":"-- # CLI Utilities","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2360"}},{"Add":{"text":"--------------------------------------------------------------------------------","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2441"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2442"}},{"Add":{"text":"namespace CliT","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2457"}},{"Add":{"text":"variable [Monad m]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2476"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2477"}},{"Add":{"text":"/-- Run the CLI on the given argument list using the given methods. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2548"}},{"Add":{"text":"def run (self : CliT m α) (args : List String) (methods : CliMethods m) : m α :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2632"}},{"Add":{"text":" ReaderT.run self methods |>.run' args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2672"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2673"}},{"Add":{"text":"/-- Get the remaining argument list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2713"}},{"Add":{"text":"def getArgs : CliT m (List String) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2751"}},{"Add":{"text":" get","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2757"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2758"}},{"Add":{"text":"/-- Replace the argument list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2792"}},{"Add":{"text":"def setArgs (args : List String) : CliT m PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2843"}},{"Add":{"text":" set args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2854"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2855"}},{"Add":{"text":"/-- Take the head of the remaining argument list (or none if empty). -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2927"}},{"Add":{"text":"def takeArg? : CliT m (Option String) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:2968"}},{"Add":{"text":" modifyGet fun | [] => (none, []) | arg :: args => (some arg, args)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3037"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3038"}},{"Add":{"text":"/-- Take the remaining argument list, leaving only an empty list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3107"}},{"Add":{"text":"def takeArgs : CliT m (List String) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3146"}},{"Add":{"text":" modifyGet fun args => (args, [])","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3181"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3182"}},{"Add":{"text":"/-- Add a string to the head of the remaining argument list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3246"}},{"Add":{"text":"def consArg (arg : String) : CliT m PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3291"}},{"Add":{"text":" modify fun args => arg :: args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3324"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3325"}},{"Add":{"text":"/-- Get the methods of this CLI. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3361"}},{"Add":{"text":"def getMethods : CliT m (CliMethods m) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3403"}},{"Add":{"text":" read >>= (·.get)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3423"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3424"}},{"Add":{"text":"/-- Change the methods of this CLI. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3463"}},{"Add":{"text":"def adaptMethods (f : CliMethods m → CliMethods m) (x : CliT m α) : CliT m α :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3547"}},{"Add":{"text":" ReaderT.adapt (fun ref => CliMethodsRef.mk <| f ref.get) x","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3609"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3610"}},{"Add":{"text":"/-- Process a short option (ex. `-x` or `--`). -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3660"}},{"Add":{"text":"def shortOption (opt : Char) : CliT m PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3707"}},{"Add":{"text":" getMethods >>= (·.shortOption opt)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3745"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3746"}},{"Add":{"text":"/-- Process a short option of the form `-x=arg`. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3798"}},{"Add":{"text":"def shortOptionEq (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3852"}},{"Add":{"text":" consArg (opt.drop 3); shortOption opt[1]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3895"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3896"}},{"Add":{"text":"/-- Process a short option of the form `-xarg`. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:3947"}},{"Add":{"text":"def shortOptionArg (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4002"}},{"Add":{"text":" consArg (opt.drop 2); shortOption opt[1]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4045"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4046"}},{"Add":{"text":"/-- Process a short option of the form `\"-x arg\"`. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4100"}},{"Add":{"text":"def shortOptionSpace (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4157"}},{"Add":{"text":" consArg <| opt.drop 2 |>.trimLeft; shortOption opt[1]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4213"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4214"}},{"Add":{"text":"/-- Process a multiple short options grouped together (ex. `-xyz` as `x`, `y`, `z`). -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4302"}},{"Add":{"text":"def multiShortOption (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4359"}},{"Add":{"text":" for i in [1:opt.length] do shortOption opt[i]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4407"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4408"}},{"Add":{"text":"/-- Process a long option (ex. `--long` or `\"--long a1 a2\"`). -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4473"}},{"Add":{"text":"def longOption (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4525"}},{"Add":{"text":" getMethods >>= (·.longOption opt)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4562"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4563"}},{"Add":{"text":"/-- Process a long short option (ex. `-long`, `-xarg`, `-xyz`). -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4630"}},{"Add":{"text":"def longShortOption (opt : String) : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4686"}},{"Add":{"text":" getMethods >>= (·.longShortOption opt)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4728"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4729"}},{"Add":{"text":"/--","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4733"}},{"Add":{"text":" Process an option, short or long.","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4769"}},{"Add":{"text":" An option is an argument of length > 1 starting with a dash (`-`).","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4838"}},{"Add":{"text":" An option may consume additional elements of the argument list.","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4904"}},{"Add":{"text":"-/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4907"}},{"Add":{"text":"def option (opt : String) : CliT m PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4951"}},{"Add":{"text":" if opt[1] == '-' then -- `--(.*)`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:4987"}},{"Add":{"text":" longOption opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5006"}},{"Add":{"text":" else","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5013"}},{"Add":{"text":" if opt.length == 2 then -- `-x`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5049"}},{"Add":{"text":" shortOption opt[1]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5074"}},{"Add":{"text":" else -- `-c(.+)`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5095"}},{"Add":{"text":" match opt[2] with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5119"}},{"Add":{"text":" | '=' => -- `-x=arg`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5146"}},{"Add":{"text":" shortOptionEq opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5172"}},{"Add":{"text":" | ' ' => -- `\"-x arg\"`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5201"}},{"Add":{"text":" shortOptionSpace opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5230"}},{"Add":{"text":" | _ => -- `-long`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5256"}},{"Add":{"text":" longShortOption opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5284"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5285"}},{"Add":{"text":"/-- Process the leading options of the remaining argument list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5352"}},{"Add":{"text":"partial def processLeadingOptions : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5407"}},{"Add":{"text":" match (← getArgs) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5434"}},{"Add":{"text":" | [] => pure ()","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5452"}},{"Add":{"text":" | arg :: args =>","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5471"}},{"Add":{"text":" let len := arg.length","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5497"}},{"Add":{"text":" if len > 1 && arg[0] == '-' then -- `-(.+)`","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5545"}},{"Add":{"text":" setArgs args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5564"}},{"Add":{"text":" option arg","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5581"}},{"Add":{"text":" processLeadingOptions","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5609"}},{"Add":{"text":" else if len == 0 then -- skip empty leading args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5662"}},{"Add":{"text":" setArgs args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5681"}},{"Add":{"text":" processLeadingOptions","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5709"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5710"}},{"Add":{"text":"/-- Process every option and collect the remaining arguments into the given `Array`. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5798"}},{"Add":{"text":"partial def collectArgsInto (arr : Array String) : CliT m (Array String) := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5877"}},{"Add":{"text":" processLeadingOptions","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5901"}},{"Add":{"text":" match (← takeArg?) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5929"}},{"Add":{"text":" | some arg => collectArgsInto (arr.push arg)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5976"}},{"Add":{"text":" | none => arr","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5992"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:5993"}},{"Add":{"text":"/-- Process every option and collect the remaining arguments into an `Array`. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6074"}},{"Add":{"text":"def collectArgs : CliT m (Array String) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6117"}},{"Add":{"text":" collectArgsInto #[]","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6139"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6140"}},{"Add":{"text":"/-- Process every option in the argument list. -/","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6190"}},{"Add":{"text":"def processOptions : CliT m PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6230"}},{"Add":{"text":" setArgs (← collectArgs).toList","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6265"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6266"}},{"Add":{"text":"end CliT","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6275"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6276"}},{"Add":{"text":"structure CliOptions where","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6303"}},{"Add":{"text":" wantsHelp : Bool := false","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6331"}},{"Add":{"text":" dir : FilePath := \".\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6355"}},{"Add":{"text":" file : FilePath := \"play.lean\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6388"}},{"Add":{"text":" subArgs : List String := []","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6418"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6419"}},{"Add":{"text":"abbrev CliM := CliT (StateT CliOptions IO)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6462"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6463"}},{"Add":{"text":"namespace CliM","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6478"}},{"Add":{"text":"open CliT","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6488"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6489"}},{"Add":{"text":"def getDir : CliM FilePath :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6519"}},{"Add":{"text":" getThe CliOptions >>= (·.dir)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6552"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6553"}},{"Add":{"text":"def setDir (dir : FilePath) : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6597"}},{"Add":{"text":" modifyThe CliOptions fun st => {st with dir := dir}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6651"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6652"}},{"Add":{"text":"def getFile : CliM FilePath :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6683"}},{"Add":{"text":" getThe CliOptions >>= (·.file)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6717"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6718"}},{"Add":{"text":"def setFile (file : FilePath) : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6764"}},{"Add":{"text":" modifyThe CliOptions fun st => {st with file := file}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6820"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6821"}},{"Add":{"text":"def getSubArgs : CliM (List String) :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6860"}},{"Add":{"text":" getThe CliOptions >>= (·.subArgs)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6897"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6898"}},{"Add":{"text":"def setSubArgs (args : List String) : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:6950"}},{"Add":{"text":" modifyThe CliOptions fun st => {st with subArgs := args}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7009"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7010"}},{"Add":{"text":"def getWantsHelp : CliM Bool :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7042"}},{"Add":{"text":" getThe CliOptions >>= (·.wantsHelp)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7081"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7082"}},{"Add":{"text":"def setWantsHelp : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7115"}},{"Add":{"text":" modifyThe CliOptions fun st => {st with wantsHelp := true}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7176"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7177"}},{"Add":{"text":"-- def getPkg (args : List String) : CliM Package := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7233"}},{"Add":{"text":"-- Package.fromDir (← getDir) args (← getFile)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7286"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7287"}},{"Add":{"text":"def takeArg : CliM String := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7319"}},{"Add":{"text":" match (← takeArg?) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7347"}},{"Add":{"text":" | none => throw <| IO.userError \"missing argument\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7400"}},{"Add":{"text":" | some arg => arg","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7420"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7421"}},{"Add":{"text":"def takeFileArg : CliM FilePath := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7459"}},{"Add":{"text":" match (← takeArg?) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7487"}},{"Add":{"text":" | none => throw <| IO.userError \"missing file argument\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7545"}},{"Add":{"text":" | some arg => arg","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7565"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7566"}},{"Add":{"text":"def unknownShortOption (opt : Char) : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7618"}},{"Add":{"text":" throw <| IO.userError s!\"unknown short option '-{opt}'\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7676"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7677"}},{"Add":{"text":"def shortOption : (opt : Char) → CliM PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7723"}},{"Add":{"text":"| 'h' => setWantsHelp","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7745"}},{"Add":{"text":"| 'd' => do setDir (← takeFileArg)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7782"}},{"Add":{"text":"| 'f' => do setFile (← takeFileArg)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7820"}},{"Add":{"text":"| opt => unknownShortOption opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7852"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7853"}},{"Add":{"text":"def unknownLongOption (opt : String) : CliM PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7906"}},{"Add":{"text":" throw <| IO.userError s!\"unknown long option '{opt}'\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7962"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:7963"}},{"Add":{"text":"def longOption : (opt : String) → CliM PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8010"}},{"Add":{"text":"| \"--help\" => setWantsHelp","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8038"}},{"Add":{"text":"| \"--dir\" => do setDir (← takeFileArg)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8081"}},{"Add":{"text":"| \"--file\" => do setFile (← takeFileArg)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8125"}},{"Add":{"text":"| \"--\" => do setSubArgs (← takeArgs)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8169"}},{"Add":{"text":"| opt => unknownLongOption opt","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8206"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8207"}},{"Add":{"text":"def command : (cmd : String) → CliM PUnit","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8251"}},{"Add":{"text":"| \"help\" => do IO.println <| help (← CliT.takeArg?)","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8312"}},{"Add":{"text":"| cmd => throw <| IO.userError s!\"unknown command '{cmd}'\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8381"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8382"}},{"Add":{"text":"def processArgs : CliM PUnit := do","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8417"}},{"Add":{"text":" match (← getArgs) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8444"}},{"Add":{"text":" | [] => IO.println usage","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8471"}},{"Add":{"text":" | [\"--version\"] => IO.println version","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8511"}},{"Add":{"text":" | _ => -- normal CLI","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8534"}},{"Add":{"text":" processOptions","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8553"}},{"Add":{"text":" match (← takeArg?) with","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8583"}},{"Add":{"text":" | none =>","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8597"}},{"Add":{"text":" if (← getWantsHelp) then IO.println usage else","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8652"}},{"Add":{"text":" throw <| IO.userError \"expected command\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8699"}},{"Add":{"text":" | some cmd =>","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8717"}},{"Add":{"text":" if (← getWantsHelp) then IO.println (help cmd) else","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8777"}},{"Add":{"text":" command cmd","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8795"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8796"}},{"Add":{"text":"def run (self : CliM PUnit) (args : List String) : IO PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8859"}},{"Add":{"text":" CliT.run self args {shortOption, longOption, longShortOption := unknownLongOption} |>.run' {}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8955"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8956"}},{"Add":{"text":"end CliM","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8965"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8966"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:8967"}},{"Add":{"text":"def cli (args : List String) : IO PUnit :=","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9010"}},{"Add":{"text":" CliM.processArgs.run args","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9038"}}]}},{"FileAdd":{"meta":{"basename":"flake.nix","metadata":0},"path":"flake.nix","context":[{"change":1,"pos":0}],"contents":[{"Add":{"text":"{","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9076"}},{"Add":{"text":" description = \"Pijul implementation in lean\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9124"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9125"}},{"Add":{"text":" inputs = {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9138"}},{"Add":{"text":" lean = {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9151"}},{"Add":{"text":" url = github:yatima-inc/lean4/acs/add-nix-ability-for-native-libs;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9224"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9231"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9232"}},{"Add":{"text":" nixpkgs.url = github:nixos/nixpkgs/nixos-21.05;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9284"}},{"Add":{"text":" flake-utils = {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9304"}},{"Add":{"text":" url = github:numtide/flake-utils;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9344"}},{"Add":{"text":" inputs.nixpkgs.follows = \"nixpkgs\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9386"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9393"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9398"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9399"}},{"Add":{"text":" outputs = { self, lean, flake-utils, nixpkgs }:","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9449"}},{"Add":{"text":" let","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9457"}},{"Add":{"text":" supportedSystems = [","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9484"}},{"Add":{"text":" # \"aarch64-linux\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9510"}},{"Add":{"text":" # \"aarch64-darwin\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9537"}},{"Add":{"text":" \"i686-linux\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9558"}},{"Add":{"text":" \"x86_64-darwin\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9582"}},{"Add":{"text":" \"x86_64-linux\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9605"}},{"Add":{"text":" ];","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9614"}},{"Add":{"text":" in","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9621"}},{"Add":{"text":" flake-utils.lib.eachSystem supportedSystems (system:","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9678"}},{"Add":{"text":" let","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9688"}},{"Add":{"text":" leanPkgs = lean.packages.${system};","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9732"}},{"Add":{"text":" pkgs = import nixpkgs { inherit system; };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9783"}},{"Add":{"text":" name = \"Pijul\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9807"}},{"Add":{"text":" project = leanPkgs.buildLeanPackage {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9853"}},{"Add":{"text":" inherit name;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9877"}},{"Add":{"text":" src = ./src;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9900"}},{"Add":{"text":" debug = true;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9924"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9935"}},{"Add":{"text":" # tests = leanPkgs.buildLeanPackage {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:9981"}},{"Add":{"text":" # name = \"Tests\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10009"}},{"Add":{"text":" # src = ./tests;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10036"}},{"Add":{"text":" # debug = true;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10062"}},{"Add":{"text":" # deps = [ leanPkgs.Lean leanPkgs.Leanpkg project ];","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10125"}},{"Add":{"text":" # nativeSharedLibs = [ (pkgs.glibc // { name = \"lib/libc-2.32.so\"; }) project.sharedLib ];","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10226"}},{"Add":{"text":" # };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10239"}},{"Add":{"text":" in","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10248"}},{"Add":{"text":" {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10256"}},{"Add":{"text":" inherit project;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10281"}},{"Add":{"text":" packages = {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10302"}},{"Add":{"text":" inherit (project) modRoot sharedLib staticLib;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10359"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10370"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10371"}},{"Add":{"text":" # checks.tests = tests;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10403"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10404"}},{"Add":{"text":" defaultPackage = project.executable;","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10449"}},{"Add":{"text":" devShell = pkgs.mkShell {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10483"}},{"Add":{"text":" buildInputs = [ leanPkgs.lean ];","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10526"}},{"Add":{"text":" LEAN_PATH = \"${leanPkgs.Lean.modRoot}\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10576"}},{"Add":{"text":" CPATH = \"${leanPkgs.Lean.modRoot}\";","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10622"}},{"Add":{"text":" };","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10633"}},{"Add":{"text":" });","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10643"}},{"Add":{"text":"}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10645"}}]}},{"FileAdd":{"meta":{"basename":"flake.lock","metadata":0},"path":"flake.lock","context":[{"change":1,"pos":0}],"contents":[{"Add":{"text":"{","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10684"}},{"Add":{"text":" \"nodes\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10697"}},{"Add":{"text":" \"flake-utils\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10718"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10736"}},{"Add":{"text":" \"lastModified\": 1634851050,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10772"}},{"Add":{"text":" \"narHash\": \"sha256-N83GlSGPJJdcqhUxSCS/WwW5pksYf3VP1M13cDRTSVA=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10846"}},{"Add":{"text":" \"owner\": \"numtide\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10874"}},{"Add":{"text":" \"repo\": \"flake-utils\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10905"}},{"Add":{"text":" \"rev\": \"c91f3de5adaf1de973b797ef7485e441a65b8935\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10964"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10989"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:10998"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11018"}},{"Add":{"text":" \"owner\": \"numtide\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11046"}},{"Add":{"text":" \"repo\": \"flake-utils\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11077"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11102"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11110"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11117"}},{"Add":{"text":" \"flake-utils_2\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11140"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11158"}},{"Add":{"text":" \"lastModified\": 1623875721,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11194"}},{"Add":{"text":" \"narHash\": \"sha256-A8BU7bjS5GirpAUv4QA+QnJ4CceLHkcXdRp4xITDB0s=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11268"}},{"Add":{"text":" \"owner\": \"numtide\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11296"}},{"Add":{"text":" \"repo\": \"flake-utils\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11327"}},{"Add":{"text":" \"rev\": \"f7e004a55b120c02ecb6219596820fcd32ca8772\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11386"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11411"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11420"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11440"}},{"Add":{"text":" \"owner\": \"numtide\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11468"}},{"Add":{"text":" \"repo\": \"flake-utils\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11499"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11524"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11532"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11539"}},{"Add":{"text":" \"lean\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11553"}},{"Add":{"text":" \"inputs\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11571"}},{"Add":{"text":" \"flake-utils\": \"flake-utils_2\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11611"}},{"Add":{"text":" \"lean-stage0\": \"lean-stage0\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11649"}},{"Add":{"text":" \"mdBook\": \"mdBook\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11677"}},{"Add":{"text":" \"nix\": \"nix\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11699"}},{"Add":{"text":" \"nixpkgs\": \"nixpkgs_2\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11731"}},{"Add":{"text":" \"temci\": \"temci\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11756"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11765"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11783"}},{"Add":{"text":" \"lastModified\": 1635858223,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11819"}},{"Add":{"text":" \"narHash\": \"sha256-kUNQsQtKpxcTE12ZfQ2jtSDxN5C5z24OY8NtJTsYJjw=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11893"}},{"Add":{"text":" \"owner\": \"yatima-inc\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11924"}},{"Add":{"text":" \"repo\": \"lean4\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:11949"}},{"Add":{"text":" \"rev\": \"3880bbb13bbc0ebcb6930fa54f088c5045a098bd\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12008"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12033"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12042"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12062"}},{"Add":{"text":" \"owner\": \"yatima-inc\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12093"}},{"Add":{"text":" \"ref\": \"acs/add-nix-ability-for-native-libs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12147"}},{"Add":{"text":" \"repo\": \"lean4\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12172"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12197"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12205"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12212"}},{"Add":{"text":" \"lean-stage0\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12233"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12251"}},{"Add":{"text":" \"lastModified\": 0,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12278"}},{"Add":{"text":" \"narHash\": \"sha256-3K/43lSW4WIHNG+HHVKCD1odS63mHuaQ4ueHyTIkcls=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12352"}},{"Add":{"text":" \"owner\": \"leanprover\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12383"}},{"Add":{"text":" \"repo\": \"lean4\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12408"}},{"Add":{"text":" \"rev\": \"0000000000000000000000000000000000000000\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12467"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12492"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12501"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12521"}},{"Add":{"text":" \"owner\": \"leanprover\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12552"}},{"Add":{"text":" \"repo\": \"lean4\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12577"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12602"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12610"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12617"}},{"Add":{"text":" \"lowdown-src\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12638"}},{"Add":{"text":" \"flake\": false,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12660"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12678"}},{"Add":{"text":" \"lastModified\": 1632391204,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12714"}},{"Add":{"text":" \"narHash\": \"sha256-zjyNA4ZmaaIbbmz2JZDqMgY7+P/uGF0nLg28Nxfg5kI=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12788"}},{"Add":{"text":" \"owner\": \"kristapsdz\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12819"}},{"Add":{"text":" \"repo\": \"lowdown\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12846"}},{"Add":{"text":" \"rev\": \"0b85e777f3cdacf4210f0d624a0ceec8df612e05\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12905"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12930"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12939"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12959"}},{"Add":{"text":" \"owner\": \"kristapsdz\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:12990"}},{"Add":{"text":" \"repo\": \"lowdown\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13017"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13042"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13050"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13057"}},{"Add":{"text":" \"mdBook\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13073"}},{"Add":{"text":" \"flake\": false,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13095"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13113"}},{"Add":{"text":" \"lastModified\": 1632991543,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13149"}},{"Add":{"text":" \"narHash\": \"sha256-Ht6aDdT5w2eEeX8Nf5kYt2/djbjDTiN0hwJBMZ91STo=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13223"}},{"Add":{"text":" \"owner\": \"leanprover\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13254"}},{"Add":{"text":" \"repo\": \"mdBook\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13280"}},{"Add":{"text":" \"rev\": \"d97081c547e96b41a9a16197882127e7e8917a3d\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13339"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13364"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13373"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13393"}},{"Add":{"text":" \"owner\": \"leanprover\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13424"}},{"Add":{"text":" \"repo\": \"mdBook\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13450"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13475"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13483"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13490"}},{"Add":{"text":" \"nix\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13503"}},{"Add":{"text":" \"inputs\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13521"}},{"Add":{"text":" \"lowdown-src\": \"lowdown-src\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13559"}},{"Add":{"text":" \"nixpkgs\": \"nixpkgs\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13588"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13597"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13615"}},{"Add":{"text":" \"lastModified\": 1632746661,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13651"}},{"Add":{"text":" \"narHash\": \"sha256-dT1hMi1Z8KQlFL589viU04vWEXpioUc3m7YGWRVwVbo=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13725"}},{"Add":{"text":" \"owner\": \"NixOS\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13751"}},{"Add":{"text":" \"repo\": \"nix\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13774"}},{"Add":{"text":" \"rev\": \"9c766a40cbbd3a350a9582d0fd8201e3361a63b2\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13833"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13858"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13867"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13887"}},{"Add":{"text":" \"owner\": \"NixOS\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13913"}},{"Add":{"text":" \"repo\": \"nix\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13936"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13961"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13969"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13976"}},{"Add":{"text":" \"nixpkgs\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:13993"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14011"}},{"Add":{"text":" \"lastModified\": 1628689438,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14047"}},{"Add":{"text":" \"narHash\": \"sha256-YMINW6YmubHZVdliGsAJpnnMYXRrvppv59LgwtnyYhs=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14121"}},{"Add":{"text":" \"owner\": \"NixOS\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14147"}},{"Add":{"text":" \"repo\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14174"}},{"Add":{"text":" \"rev\": \"f6551e1efa261568c82b76c3a582b2c2ceb1f53f\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14233"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14258"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14267"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14287"}},{"Add":{"text":" \"id\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14312"}},{"Add":{"text":" \"ref\": \"nixos-21.05-small\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14348"}},{"Add":{"text":" \"type\": \"indirect\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14375"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14383"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14390"}},{"Add":{"text":" \"nixpkgs_2\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14409"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14427"}},{"Add":{"text":" \"lastModified\": 1633329294,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14463"}},{"Add":{"text":" \"narHash\": \"sha256-0LpQLS4KMgxslMgmDHmxG/5twFlXDBW9z4Or1iOrCvU=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14537"}},{"Add":{"text":" \"owner\": \"NixOS\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14563"}},{"Add":{"text":" \"repo\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14590"}},{"Add":{"text":" \"rev\": \"ee084c02040e864eeeb4cf4f8538d92f7c675671\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14649"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14674"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14683"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14703"}},{"Add":{"text":" \"owner\": \"NixOS\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14729"}},{"Add":{"text":" \"ref\": \"nixpkgs-unstable\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14764"}},{"Add":{"text":" \"repo\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14791"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14816"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14824"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14831"}},{"Add":{"text":" \"nixpkgs_3\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14850"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14868"}},{"Add":{"text":" \"lastModified\": 1635719588,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14904"}},{"Add":{"text":" \"narHash\": \"sha256-pWjdy0NheM97NsPE6+jUnr5LYyeA0sBGTdw4mfXMGZQ=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:14978"}},{"Add":{"text":" \"owner\": \"nixos\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15004"}},{"Add":{"text":" \"repo\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15031"}},{"Add":{"text":" \"rev\": \"f0869b1a2c0b150aac26e10bb5c2364ffb2e804f\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15090"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15115"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15124"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15144"}},{"Add":{"text":" \"owner\": \"nixos\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15170"}},{"Add":{"text":" \"ref\": \"nixos-21.05\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15200"}},{"Add":{"text":" \"repo\": \"nixpkgs\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15227"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15252"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15260"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15267"}},{"Add":{"text":" \"root\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15281"}},{"Add":{"text":" \"inputs\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15299"}},{"Add":{"text":" \"flake-utils\": \"flake-utils\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15337"}},{"Add":{"text":" \"lean\": \"lean\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15361"}},{"Add":{"text":" \"nixpkgs\": \"nixpkgs_3\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15392"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15400"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15407"}},{"Add":{"text":" \"temci\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15422"}},{"Add":{"text":" \"flake\": false,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15444"}},{"Add":{"text":" \"locked\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15462"}},{"Add":{"text":" \"lastModified\": 1626860219,","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15498"}},{"Add":{"text":" \"narHash\": \"sha256-rFJb+M3ru2shqxpsZfiAFLFfc38dFaF7u2T88pvG14M=\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15572"}},{"Add":{"text":" \"owner\": \"parttimenerd\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15605"}},{"Add":{"text":" \"repo\": \"temci\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15630"}},{"Add":{"text":" \"rev\": \"fe4f47173a27cf75f734502fcb88d3d0a3860dca\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15689"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15714"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15723"}},{"Add":{"text":" \"original\": {","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15743"}},{"Add":{"text":" \"owner\": \"parttimenerd\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15776"}},{"Add":{"text":" \"repo\": \"temci\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15801"}},{"Add":{"text":" \"type\": \"github\"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15826"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15834"}},{"Add":{"text":" }","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15840"}},{"Add":{"text":" },","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15845"}},{"Add":{"text":" \"root\": \"root\",","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15863"}},{"Add":{"text":" \"version\": 7","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15878"}},{"Add":{"text":"}","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15880"}}]}},{"FileAdd":{"meta":{"basename":"README.md","metadata":0},"path":"README.md","context":[{"change":1,"pos":0}],"contents":[{"Add":{"text":"# Pijul.lean","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15929"}},{"Add":{"text":"","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15930"}},{"Add":{"text":"A non-serious attempt to implement Pijul in Lean4.","pos":"DOVIOWRFFIG6HCDZMS5E6I3DPYGDYVHMF4YYK6FKFMAMC3E5ZA3AC:15981"}}]}}],"owner":"Anderssorby","repo":"Pijul.lean","login":null}

…

Dependencies

Change contents

Review